Concrete Binary Tower Field

Field-structure lemmas for successive levels of the concrete binary tower. The field dictionary uses binary natural powers and integer powers that invert the natural-power result for negative exponents. The named raw binary-power routine agrees with field powers.

Norm nonvanishing is certified using QuadraticAlgebra.norm_eq_zero_iff_eq_zero over the predecessor field. This argument does not assume a field structure on the successor level.

Lemmas of field properties at level k that depends on field properties at level (k-1)

theorem ConcreteBinaryTower.concrete_mul_eq {k : ℕ} {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a b : ConcreteBTField k) {a₁ a₀ b₁ b₀ : ConcreteBTField (k - 1)} (h_a : (a₁, a₀) = split h_k a) (h_b : (b₁, b₀) = split h_k b) : concrete_mul a b = join h_k (concrete_mul a₀ b₁ + concrete_mul b₀ a₁ + concrete_mul (concrete_mul a₁ b₁) (Z (k - 1))) (concrete_mul a₀ b₀ + concrete_mul a₁ b₁)

theorem ConcreteBinaryTower.concrete_zero_mul {k : ℕ} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a : ConcreteBTField k) : concrete_mul zero a = zero

theorem ConcreteBinaryTower.concrete_mul_zero {k : ℕ} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a : ConcreteBTField k) : concrete_mul a zero = zero

theorem ConcreteBinaryTower.concrete_one_mul {k : ℕ} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a : ConcreteBTField k) : concrete_mul one a = a

theorem ConcreteBinaryTower.concrete_mul_one {k : ℕ} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a : ConcreteBTField k) : concrete_mul a one = a

theorem ConcreteBinaryTower.concrete_pow_base_one {k : ℕ} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (n : ℕ) : concrete_pow_nat 1 n = 1

theorem ConcreteBinaryTower.concrete_mul_comm {k : ℕ} {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a b : ConcreteBTField k) : concrete_mul a b = concrete_mul b a

theorem ConcreteBinaryTower.concrete_mul_assoc {k : ℕ} {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a b c : ConcreteBTField k) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)

The recursive multiplication is associative at a positive level whenever the predecessor level satisfies its field laws.

theorem ConcreteBinaryTower.concrete_mul_left_distrib {k : ℕ} {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a b c : ConcreteBTField k) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c

At a positive level, recursive multiplication distributes over addition in its second argument whenever the predecessor level satisfies its field laws.

theorem ConcreteBinaryTower.concrete_mul_right_distrib {k : ℕ} {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k - 1)) (a b c : ConcreteBTField k) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c

theorem ConcreteBinaryTower.norm_of_ne_zero_is_ne_zero {k : ℕ} {h_k_gt_0 : k > 0} (prevBTFieldResult : ConcreteBTFStepResult (k - 1)) (a : ConcreteBTField k) (h_a_ne_zero : a ≠ 0) : have a₁ := (split h_k_gt_0 a).1; have a₀ := (split h_k_gt_0 a).2; concrete_mul a₀ (a₀ + concrete_mul a₁ (Z (k - 1))) + concrete_mul a₁ a₁ ≠ 0

For a nonzero element at a positive level, lo * (lo + hi * z) + hi * hi is nonzero in the predecessor field, where lo and hi are its low and high halves and z = Z (k - 1). This is the denominator in the quadratic inverse formula.

theorem ConcreteBinaryTower.concrete_mul_inv_cancel {k : ℕ} (prevBTFieldResult : ConcreteBTFStepResult (k - 1)) (a : ConcreteBTField k) (h : a ≠ 0) : concrete_mul a (concrete_inv a) = one

theorem ConcreteBinaryTower.concrete_inv_one {k : ℕ} : concrete_inv 1 = 1

Inductive tower construction, using lemmas from BTFieldPropsOneLevelLiftingLemmas

theorem ConcreteBinaryTower.Z_square_eq (k : ℕ) (prevBTFieldProps : ConcreteBTFieldProps k) (curBTFieldProps : ConcreteBTFieldProps (k + 1)) : Z (k + 1) ^ 2 = join ⋯ (Z k) 1

theorem ConcreteBinaryTower.liftBTFieldProps (k : ℕ) (prevBTFResult : ConcreteBTFStepResult k) : ConcreteBTFieldProps (k + 1)

@[reducible]

def ConcreteBinaryTower.liftConcreteBTField (k : ℕ) (prevBTFResult : ConcreteBTFStepResult k) : Field (ConcreteBTField (k + 1))

def ConcreteBinaryTower.concreteCanonicalEmbedding (k : ℕ) (prevBTFieldProps : ConcreteBTFieldProps k) (curBTFieldProps : ConcreteBTFieldProps (k + 1)) : ConcreteBTField k →+* ConcreteBTField (k + 1)

The canonical ring homomorphism embedding ConcreteBTField k into ConcreteBTField (k + 1). This is the AdjoinRoot.of map.

@[instance_reducible]

instance ConcreteBinaryTower.instAlgebraLiftConcreteBTField (k : ℕ) (prevBTFResult : ConcreteBTFStepResult k) : Algebra (ConcreteBTField k) (ConcreteBTField (k + 1))

theorem ConcreteBinaryTower.Z_square_mul_form (k : ℕ) (prev : ConcreteBTFStepResult k) : Z (k + 1) ^ 2 = Z (k + 1) * (algebraMap (ConcreteBTField k) (ConcreteBTField (k + 1))) (Z k) + 1

theorem ConcreteBinaryTower.sum_inv_Z_next_eq (k : ℕ) (prev : ConcreteBTFStepResult k) : Z (k + 1) + (Z (k + 1))⁻¹ = (algebraMap (ConcreteBTField k) (ConcreteBTField (k + 1))) (Z k)

noncomputable def ConcreteBinaryTower.getBTFResult (k : ℕ) : ConcreteBTFStepResult k

@[instance_reducible]

instance ConcreteBinaryTower.instFieldConcrete {k : ℕ} : Field (ConcreteBTField k)

theorem ConcreteBinaryTower.npow_def {k : ℕ} (a : ConcreteBTField k) (n : ℕ) : a ^ n = npowBinRec n a

Natural powers use binary exponentiation of the concrete multiplication.

theorem ConcreteBinaryTower.zpow_def {k : ℕ} (a : ConcreteBTField k) (n : ℤ) : a ^ n = zpowRec npowBinRec n a

Integer powers use binary exponentiation, followed by inversion for negative exponents.

theorem ConcreteBinaryTower.concrete_pow_nat_eq_pow {k : ℕ} (a : ConcreteBTField k) (n : ℕ) : concrete_pow_nat a n = a ^ n

The raw binary-power routine agrees with natural powers in the field.

instance ConcreteBinaryTower.instCharP2 {k : ℕ} : CharP (ConcreteBTField k) 2

@[instance_reducible]

noncomputable instance ConcreteBinaryTower.instFintype {k : ℕ} : Fintype (ConcreteBTField k)

def ConcreteBinaryTower.𝕏 (k : ℕ) : ConcreteBTField (k + 1)

adjoined root of poly k, generator of successor field BTField (k + 1)