Binary Tower Preliminaries

Shared finite-field and bitwise preliminaries for the binary tower development.

def «termGF(_)» : Lean.ParserDescr

@[implicit_reducible]

noncomputable 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 sum_Icc_shift {M : Type u_1} [AddCommMonoid M] (f : ℕ → M) (a b shift : ℕ) : ∑ j ∈ Finset.Icc a b, f (j + shift) = ∑ j ∈ Finset.Icc (a + shift) (b + shift), f j

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