Prelude for Binary Tower Fields

This file contains preliminary definitions, theorems, instances that are used in defining BTFs

def «termGF(_)» : Lean.ParserDescr

instance GF_2_fintype : Fintype (GF(2))

theorem GF_2_pow_card (x : GF(2)) : x ^ Fintype.card (GF(2)) = x

theorem GF_2_card : Fintype.card (GF(2)) = 2 ^ 2 ^ 0

theorem non_zero_divisors_iff (M₀ : Type u_1) [Mul M₀] [Zero M₀] : NoZeroDivisors M₀ ↔ ∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0

instance neZero_one_of_nontrivial_comm_monoid_zero {M₀ : Type u_1} [CommMonoidWithZero M₀] [instNontrivial : Nontrivial M₀] : NeZero 1

instance unit_of_nontrivial_comm_monoid_with_zero_is_not_zero {R : Type u_1} [CommMonoidWithZero R] [Nontrivial R] {a : R} (h_unit : IsUnit a) : NeZero a

theorem GF_2_value_eq_zero_or_one (x : GF(2)) : x = 0 ∨ x = 1

Any element in GF(2) is either 0 or 1.

theorem GF_2_one_add_one_eq_zero : 1 + 1 = 0

theorem withBot_lt_one_cases (x : WithBot ℕ) (h : x < ↑1) : x = ⊥ ∨ x = ↑0

theorem is_unit_iff_deg_0 {R : Type u_1} [Field R] {p : Polynomial R} : p.degree = 0 ↔ IsUnit p

theorem non_trivial_factors_of_non_trivial_poly_have_deg_ge_1 {R : Type u_1} [Field R] {p a b : Polynomial R} (h_prod : p = a * b) (h_p_nonzero : p ≠ 0) (h_a_non_unit : ¬IsUnit a) (h_b_non_unit : ¬IsUnit b) : 1 ≤ a.degree ∧ 1 ≤ b.degree

theorem prod_univ_twos {M : Type u_1} [CommMonoid M] {n : ℕ} (hn : n = 2) (f : Fin n → M) : ∏ i : Fin n, f i = f (Fin.cast ⋯ 0) * f (Fin.cast ⋯ 1)

theorem sum_univ_twos {M : Type u_1} [AddCommMonoid M] {n : ℕ} (hn : n = 2) (f : Fin n → M) : ∑ i : Fin n, f i = f (Fin.cast ⋯ 0) + f (Fin.cast ⋯ 1)

theorem unique_repr {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] [Algebra R S] (pb : PowerBasis R S) (repr1 repr2 : Fin pb.dim →₀ R) (h : ∑ i : Fin pb.dim, repr1 i • pb.basis i = ∑ i : Fin pb.dim, repr2 i • pb.basis i) : repr1 = repr2

theorem linear_sum_repr (R : Type u_1) [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] (pb : PowerBasis R S) (h_dim : pb.dim = 2) (s : S) : ∃ (a : R) (b : R), s = a • pb.gen + (algebraMap R S) b

theorem unique_linear_sum_repr (R : Type u_1) [CommRing R] (S : Type u_2) [CommRing S] [Algebra R S] (pb : PowerBasis R S) (h_dim : pb.dim = 2) (s : S) : ∃! p : R × R, s = p.1 • pb.gen + (algebraMap R S) p.2

theorem linear_form_of_elements_in_adjoined_commring {R : Type u_1} [CommRing R] (f : Polynomial R) (hf_deg : f.natDegree = 2) (hf_monic : f.Monic) (c1 : AdjoinRoot f) : ∃ (a : R) (b : R), c1 = (AdjoinRoot.of f) a * AdjoinRoot.root f + (AdjoinRoot.of f) b

theorem unique_linear_form_of_elements_in_adjoined_commring {R : Type u_1} [CommRing R] (f : Polynomial R) (hf_deg : f.natDegree = 2) (hf_monic : f.Monic) (c1 : AdjoinRoot f) : ∃! p : R × R, c1 = (AdjoinRoot.of f) p.1 * AdjoinRoot.root f + (AdjoinRoot.of f) p.2

structure GaloisAutomorphism (F : Type u_1) [Field F] (u : F) (k : ℕ) : Prop

Galois automorphism properties for a special element in a binary tower field. Encapsulates the key relationship : u^(2^(2^k)) = u⁻¹ and (u⁻¹)^(2^(2^k)) = u

• forward : u ^ 2 ^ 2 ^ k = u⁻¹
• reverse : u⁻¹ ^ 2 ^ 2 ^ k = u

structure TraceMapProperty (F : Type u_1) [Field F] (u : F) (k : ℕ) : Prop

Trace map properties for elements in a binary tower field extension. Asserts that the trace of both an element and its inverse equals 1.

• element_trace : ∑ i ∈ Finset.range (2 ^ k), u ^ 2 ^ i = 1
• inverse_trace : ∑ i ∈ Finset.range (2 ^ k), u⁻¹ ^ 2 ^ i = 1

structure SpecialElementRelation {F_prev : Type u_1} [Field F_prev] (t1 : F_prev) {F_cur : Type u_2} [Field F_cur] (u : F_cur) [Algebra F_prev F_cur] : Prop

Special element relationship in binary tower fields. Captures the key equation : u + u⁻¹ = t₁ (lifted previous special element)

• sum_inv_eq : u + u⁻¹ = (algebraMap F_prev F_cur) t1
• h_u_square : u ^ 2 = u * (algebraMap F_prev F_cur) t1 + 1

theorem two_eq_zero_in_char2_field {F : Type u_1} [Field F] (sumZeroIffEq : ∀ (x y : F), x + y = 0 ↔ x = y) : 2 = 0

theorem sum_of_pow_exp_of_2 {F : Type u_1} [Field F] (sumZeroIffEq : ∀ (x y : F), x + y = 0 ↔ x = y) (i : ℕ) (a b c : F) : a + b = c → a ^ 2 ^ i + b ^ 2 ^ i = c ^ 2 ^ i

theorem sum_square_char2 {F : Type u_1} [Field F] (sumZeroIffEq : ∀ (x y : F), x + y = 0 ↔ x = y) (s : Finset ℕ) (f : ℕ → F) : (∑ j ∈ s, f j) ^ 2 = ∑ j ∈ s, f j ^ 2

theorem singleton_subset_Icc (n : ℕ) : {1} ⊆ Finset.Icc 1 (n + 1)

theorem two_le_two_pow_n_plus_1 (n : ℕ) : 2 ≤ 2 ^ (n + 1)

theorem one_le_two_pow_n (n : ℕ) : 1 ≤ 2 ^ n

theorem zero_lt_pow_n (m n : ℕ) (h_m : m > 0) : 0 < m ^ n

theorem one_le_sub_consecutive_two_pow (n : ℕ) : 1 ≤ 2 ^ (n + 1) - 2 ^ n

theorem two_pow_ne_zero (n : ℕ) : 2 ^ n ≠ 0

theorem pow_exp_of_2_repr_given_x_square_repr {F : Type u_1} [instField : Field F] (sumZeroIffEq : ∀ (x y : F), x + y = 0 ↔ x = y) (x z : F) (h_z_non_zero : z ≠ 0) (h_x_square : x ^ 2 = x * z + 1) (i : ℕ) : x ^ 2 ^ i = x * z ^ (2 ^ i - 1) + ∑ j ∈ Finset.Icc 1 i, z ^ (2 ^ i - 2 ^ j)

For any field element (x : F) where x^2 = x*z + 1, this theorem gives a closed form for x^(2^i)

theorem inverse_is_root_of_prevPoly {prevBTField : Type u_1} [Field prevBTField] {curBTField : Type u_2} [Field curBTField] (of_prev : prevBTField →+* curBTField) (u : curBTField) (t1 : prevBTField) (specialElementNeZero : u ≠ 0) (eval_prevPoly_at_root : u ^ 2 + of_prev t1 * u + 1 = 0) (h_eval : ∀ (x : curBTField), Polynomial.eval₂ of_prev x (Polynomial.X ^ 2 + (Polynomial.C t1 * Polynomial.X + 1)) = x ^ 2 + of_prev t1 * x + 1) : Polynomial.eval₂ of_prev u⁻¹ (Polynomial.X ^ 2 + (Polynomial.C t1 * Polynomial.X + 1)) = 0

theorem sum_of_root_and_inverse_is_t1 {curBTField : Type u_1} [Field curBTField] (u t1 : curBTField) (specialElementNeZero : u ≠ 0) (eval_prevPoly_at_root : u ^ 2 + t1 * u + 1 = 0) (sumZeroIffEq : ∀ (x y : curBTField), x + y = 0 ↔ x = y) : u + u⁻¹ = t1

theorem self_sum_eq_zero {prevBTField : Type u_1} [CommRing prevBTField] (sumZeroIffEqPrev : ∀ (x y : prevBTField), x + y = 0 ↔ x = y) (prevPoly : Polynomial prevBTField) (hf_deg : prevPoly.natDegree = 2) (hf_monic : prevPoly.Monic) (x : AdjoinRoot prevPoly) : x + x = 0

theorem sum_zero_iff_eq_of_self_sum_zero {F : Type u_1} [AddGroup F] (h_self_sum_eq_zero : ∀ (x : F), x + x = 0) (x y : F) : x + y = 0 ↔ x = y

theorem prod_mul_erase {α : Type u_1} {β : Type u_2} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) : f a * ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x

A variant of Finset.mul_prod_erase with the multiplication swapped.

theorem sum_add_erase {α : Type u_1} {β : Type u_2} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) : f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x

A variant of Finset.add_sum_erase with the addition swapped.-

theorem eval₂_quadratic_prevField_coeff {prevBTField : Type u_1} [CommRing prevBTField] {curBTField : Type u_2} [CommRing curBTField] (of_prev : prevBTField →+* curBTField) (t1 : prevBTField) (x : curBTField) : Polynomial.eval₂ of_prev x (Polynomial.X ^ 2 + (Polynomial.C t1 * Polynomial.X + 1)) = x ^ 2 + of_prev t1 * x + 1

theorem galois_eval_in_BTField {curBTField : Type u_1} [Field curBTField] (u t1 : curBTField) (k : ℕ) (sumZeroIffEq : ∀ (x y : curBTField), x + y = 0 ↔ x = y) (prevSpecialElementNeZero : t1 ≠ 0) (u_plus_inv_eq_t1 : u + u⁻¹ = t1) (h_u_square : u ^ 2 = u * t1 + 1) (h_t1_pow : t1 ^ (2 ^ 2 ^ k - 1) = 1 ∧ t1⁻¹ ^ (2 ^ 2 ^ k - 1) = 1) (h_t1_pow_2_pow_2_pow_k : t1 ^ 2 ^ 2 ^ k = t1) (h_t1_inv_pow_2_pow_2_pow_k : t1⁻¹ ^ 2 ^ 2 ^ k = t1⁻¹) (trace_map_at_inv : ∑ i ∈ Finset.range (2 ^ k), t1⁻¹ ^ 2 ^ i = 1) : u ^ 2 ^ 2 ^ k = u⁻¹

theorem galois_automorphism_power {curBTField : Type u_1} [Field curBTField] (u t1 : curBTField) (k : ℕ) (sumZeroIffEq : ∀ (x y : curBTField), x + y = 0 ↔ x = y) (specialElementNeZero : u ≠ 0) (prevSpecialElementNeZero : t1 ≠ 0) (u_plus_inv_eq_t1 : u + u⁻¹ = t1) (h_u_square : u ^ 2 = u * t1 + 1) (h_t1_pow : t1 ^ (2 ^ 2 ^ k - 1) = 1 ∧ t1⁻¹ ^ (2 ^ 2 ^ k - 1) = 1) (trace_map_roots : ∑ i ∈ Finset.range (2 ^ k), t1 ^ 2 ^ i = 1 ∧ ∑ i ∈ Finset.range (2 ^ k), t1⁻¹ ^ 2 ^ i = 1) : u ^ 2 ^ 2 ^ k = u⁻¹ ∧ u⁻¹ ^ 2 ^ 2 ^ k = u

theorem lifted_trace_map_eval_at_roots_prev_BTField {curBTField : Type u_1} [Field curBTField] (u t1 : curBTField) (k : ℕ) (sumZeroIffEq : ∀ (x y : curBTField), x + y = 0 ↔ x = y) (u_plus_inv_eq_t1 : u + u⁻¹ = t1) (galois_automorphism : u ^ 2 ^ 2 ^ k = u⁻¹ ∧ u⁻¹ ^ 2 ^ 2 ^ k = u) (trace_map_at_prev_root : ∑ i ∈ Finset.range (2 ^ k), t1 ^ 2 ^ i = 1) : ∑ i ∈ Finset.range (2 ^ (k + 1)), u ^ 2 ^ i = 1

theorem rsum_eq_t1_square_aux {curBTField : Type u_1} [Field curBTField] (u : curBTField) (k : ℕ) (x_pow_card : ∀ (x : curBTField), x ^ 2 ^ 2 ^ k = x) (u_ne_zero : u ≠ 0) (trace_map_prop : TraceMapProperty curBTField u k) : ∑ j ∈ Finset.Icc 1 (2 ^ k), u ^ (2 ^ 2 ^ k - 2 ^ j) = u

instance charP_eq_2_of_add_self_eq_zero {F : Type u_1} [Field F] (sumZeroIffEq : ∀ (x y : F), x + y = 0 ↔ x = y) : CharP F 2

@[simp]

theorem bit_finProdFinEquiv_symm_2_pow_succ {n : ℕ} (j : Fin (2 ^ (n + 1))) (i : Fin (n + 1)) : have e := finProdFinEquiv.symm; (↑i).getBit ↑j = if ↑i > 0 then (↑i - 1).getBit ↑(e j).1 else ↑(e j).2

def leftDivNat {m n : ℕ} (i : Fin (m * n)) : Fin n

Equivalence between Fin m × Fin n and Fin (m * n) which splits quotient part into Fin (n) and the remainder into Fin (m). If m and n are powers of 2, the Fin (n) holds MSBs and Fin (m) holds LSBs. This is a reversed version of finProdFinEquiv. We put m before n for integration with Basis.smulTower in multilinearBasis though it's a bit counter-intuitive.

def leftModNat {m n : ℕ} (h_m : m > 0) (i : Fin (m * n)) : Fin m

def revFinProdFinEquiv {m n : ℕ} (h_m : m > 0) : Fin m × Fin n ≃ Fin (m * n)

@[simp]

theorem revFinProdFinEquiv_apply_val {m n : ℕ} (h_m : m > 0) (x : Fin m × Fin n) : ↑((revFinProdFinEquiv h_m) x) = ↑x.1 + m * ↑x.2

@[simp]

theorem revFinProdFinEquiv_symm_apply {m n : ℕ} (h_m : m > 0) (x : Fin (m * n)) : (revFinProdFinEquiv h_m).symm x = (leftModNat h_m x, leftDivNat x)

@[simp]

theorem bit_revFinProdFinEquiv_symm_2_pow_succ {n : ℕ} (j : Fin (2 ^ (n + 1))) (i : Fin (n + 1)) : have e := (revFinProdFinEquiv ⋯).symm; have msb := (e j).2; have lsbs := (e j).1; (↑i).getBit ↑j = if ↑i < n then (↑i).getBit ↑lsbs else ↑msb

theorem linearIndependent_fin2' {K : Type u_3} {V : Type u} [DivisionRing K] [AddCommGroup V] [Module K V] {f : Fin 2 → V} : LinearIndependent K f ↔ f 0 ≠ 0 ∧ ∀ (a : K), a • f 0 ≠ f 1

noncomputable def definingPoly {F : Type u_1} [instField : Field F] (s : F) : Polynomial F

theorem degree_s_smul_X {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] : (Polynomial.C s * Polynomial.X).degree = 1

theorem degree_s_smul_X_add_1 {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] : (Polynomial.C s * Polynomial.X + 1).degree = 1

theorem definingPoly_is_monic {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] : (definingPoly s).Monic

theorem degree_definingPoly {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] : (definingPoly s).degree = 2

theorem natDegree_definingPoly {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] : (definingPoly s).natDegree = 2

theorem definingPoly_ne_zero {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] : definingPoly s ≠ 0

theorem definingPoly_is_not_unit {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] : ¬IsUnit (definingPoly s)

theorem definingPoly_coeffOf0 {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] : (definingPoly s).coeff 0 = 1

theorem definingPoly_coeffOf1 {F : Type u_1} [Field F] [Fintype F] (s : F) [NeZero s] : (definingPoly s).coeff 1 = s

theorem traceMapProperty_of_quadratic_extension (F_prev : Type u_1) [Field F_prev] [Fintype F_prev] (k : ℕ) (fintypeCardPrev : Fintype.card F_prev = 2 ^ 2 ^ k) (t1 : F_prev) [instNeZero_t1 : NeZero t1] {F_cur : Type u_2} [Field F_cur] (u : F_cur) [instNeZero_u : NeZero u] [Algebra F_prev F_cur] (h_rel : SpecialElementRelation t1 u) (prev_trace_map : TraceMapProperty F_prev t1 k) (sumZeroIffEq : ∀ (x y : F_cur), x + y = 0 ↔ x = y) : TraceMapProperty F_cur u (k + 1)

Instance : The trace map property for a quadratic extension defined by a root u of X^2 + t1 * X + 1, assuming the trace property for t1 at the previous level.

theorem not_irreducible_of_isRoot_of_degree_gt_one {R : Type u_1} [CommRing R] [IsDomain R] (p : Polynomial R) (h_root : ∃ (r : R), p.IsRoot r) (h_deg : p.degree > 1) : ¬Irreducible p

A polynomial with a degree greater than 1 is not irreducible if it has a root in R.