Concrete binary tower field construction interface

Compatibility entry point for the executable arithmetic, together with the law records, finite-field utilities, and field-instance assembly used by the recursive construction. Arithmetic-only clients can import CompPoly.Fields.Binary.Tower.Concrete.Arithmetic; canonical field clients use CompPoly.Fields.Binary.Tower.Concrete.Field.

@[instance_reducible]

noncomputable instance ConcreteBinaryTower.instDecidableEqGaloisFieldOfNatNat_compPoly : DecidableEq (GF(2))

noncomputable def ConcreteBinaryTower.toConcreteBTF0 : GF(2) → ConcreteBTField 0

noncomputable def ConcreteBinaryTower.fromConcreteBTF0 : ConcreteBTField 0 → (GF(2))

def ConcreteBinaryTower.coeffsToBitVec {n : ℕ} (coeffs : List (ZMod 2)) : BitVec n

structure ConcreteBinaryTower.ConcreteBTFAddCommGroupProps (k : ℕ) : Prop

• add_assoc (a b c : ConcreteBTField k) : a + b + c = a + (b + c)
• add_comm (a b : ConcreteBTField k) : a + b = b + a
• add_zero (a : ConcreteBTField k) : a + zero = a
• zero_add (a : ConcreteBTField k) : zero + a = a
• add_neg (a : ConcreteBTField k) : a + neg a = zero

structure ConcreteBinaryTower.ConcreteBTFRingProps (k : ℕ) extends ConcreteBinaryTower.ConcreteBTFAddCommGroupProps k : Prop

• add_assoc (a b c : ConcreteBTField k) : a + b + c = a + (b + c)
• add_comm (a b : ConcreteBTField k) : a + b = b + a
• add_zero (a : ConcreteBTField k) : a + zero = a
• zero_add (a : ConcreteBTField k) : zero + a = a
• add_neg (a : ConcreteBTField k) : a + neg a = zero
• mul_eq (a b : ConcreteBTField k) (h_k : k > 0) {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₁)
• zero_mul (a : ConcreteBTField k) : concrete_mul zero a = zero
• zero_mul' (a : ConcreteBTField k) : concrete_mul 0 a = 0
• mul_zero (a : ConcreteBTField k) : concrete_mul a zero = zero
• mul_zero' (a : ConcreteBTField k) : concrete_mul a 0 = 0
• one_mul (a : ConcreteBTField k) : concrete_mul one a = a
• mul_one (a : ConcreteBTField k) : concrete_mul a one = a
• mul_assoc (a b c : ConcreteBTField k) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)
• mul_left_distrib (a b c : ConcreteBTField k) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c
• mul_right_distrib (a b c : ConcreteBTField k) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c

structure ConcreteBinaryTower.ConcreteBTFDivisionRingProps (k : ℕ) extends ConcreteBinaryTower.ConcreteBTFRingProps k : Prop

• add_assoc (a b c : ConcreteBTField k) : a + b + c = a + (b + c)
• add_comm (a b : ConcreteBTField k) : a + b = b + a
• add_zero (a : ConcreteBTField k) : a + zero = a
• zero_add (a : ConcreteBTField k) : zero + a = a
• add_neg (a : ConcreteBTField k) : a + neg a = zero
• mul_eq (a b : ConcreteBTField k) (h_k : k > 0) {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₁)
• zero_mul (a : ConcreteBTField k) : concrete_mul zero a = zero
• zero_mul' (a : ConcreteBTField k) : concrete_mul 0 a = 0
• mul_zero (a : ConcreteBTField k) : concrete_mul a zero = zero
• mul_zero' (a : ConcreteBTField k) : concrete_mul a 0 = 0
• one_mul (a : ConcreteBTField k) : concrete_mul one a = a
• mul_one (a : ConcreteBTField k) : concrete_mul a one = a
• mul_assoc (a b c : ConcreteBTField k) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)
• mul_left_distrib (a b c : ConcreteBTField k) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c
• mul_right_distrib (a b c : ConcreteBTField k) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c
• mul_inv_cancel (a : ConcreteBTField k) : a ≠ zero → concrete_mul a (concrete_inv a) = one

structure ConcreteBinaryTower.ConcreteBTFieldProps (k : ℕ) extends ConcreteBinaryTower.ConcreteBTFDivisionRingProps k : Prop

• add_assoc (a b c : ConcreteBTField k) : a + b + c = a + (b + c)
• add_comm (a b : ConcreteBTField k) : a + b = b + a
• add_zero (a : ConcreteBTField k) : a + zero = a
• zero_add (a : ConcreteBTField k) : zero + a = a
• add_neg (a : ConcreteBTField k) : a + neg a = zero
• mul_eq (a b : ConcreteBTField k) (h_k : k > 0) {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₁)
• zero_mul (a : ConcreteBTField k) : concrete_mul zero a = zero
• zero_mul' (a : ConcreteBTField k) : concrete_mul 0 a = 0
• mul_zero (a : ConcreteBTField k) : concrete_mul a zero = zero
• mul_zero' (a : ConcreteBTField k) : concrete_mul a 0 = 0
• one_mul (a : ConcreteBTField k) : concrete_mul one a = a
• mul_one (a : ConcreteBTField k) : concrete_mul a one = a
• mul_assoc (a b c : ConcreteBTField k) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)
• mul_left_distrib (a b c : ConcreteBTField k) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c
• mul_right_distrib (a b c : ConcreteBTField k) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c
• mul_inv_cancel (a : ConcreteBTField k) : a ≠ zero → concrete_mul a (concrete_inv a) = one
• mul_comm (a b : ConcreteBTField k) : concrete_mul a b = concrete_mul b a

@[reducible]

def ConcreteBinaryTower.mkRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Ring (ConcreteBTField k)

@[reducible]

def ConcreteBinaryTower.mkDivisionRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : DivisionRing (ConcreteBTField k)

@[reducible]

def ConcreteBinaryTower.mkFieldInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Field (ConcreteBTField k)

structure ConcreteBinaryTower.ConcreteBTFStepResult (k : ℕ) extends ConcreteBinaryTower.ConcreteBTFieldProps k : Type

• add_assoc (a b c : ConcreteBTField k) : a + b + c = a + (b + c)
• add_comm (a b : ConcreteBTField k) : a + b = b + a
• add_zero (a : ConcreteBTField k) : a + zero = a
• zero_add (a : ConcreteBTField k) : zero + a = a
• add_neg (a : ConcreteBTField k) : a + neg a = zero
• mul_eq (a b : ConcreteBTField k) (h_k : k > 0) {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₁)
• zero_mul (a : ConcreteBTField k) : concrete_mul zero a = zero
• zero_mul' (a : ConcreteBTField k) : concrete_mul 0 a = 0
• mul_zero (a : ConcreteBTField k) : concrete_mul a zero = zero
• mul_zero' (a : ConcreteBTField k) : concrete_mul a 0 = 0
• one_mul (a : ConcreteBTField k) : concrete_mul one a = a
• mul_one (a : ConcreteBTField k) : concrete_mul a one = a
• mul_assoc (a b c : ConcreteBTField k) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)
• mul_left_distrib (a b c : ConcreteBTField k) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c
• mul_right_distrib (a b c : ConcreteBTField k) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c
• mul_inv_cancel (a : ConcreteBTField k) : a ≠ zero → concrete_mul a (concrete_inv a) = one
• mul_comm (a b : ConcreteBTField k) : concrete_mul a b = concrete_mul b a
• instFintype : Fintype (ConcreteBTField k)
• fieldFintypeCard : Fintype.card (ConcreteBTField k) = 2 ^ 2 ^ k
• sumZeroIffEq (x y : ConcreteBTField k) : x + y = 0 ↔ x = y
• traceMapEvalAtRootsIs1 : TraceMapProperty (ConcreteBTField k) (Z k) k
• instIrreduciblePoly : Irreducible (definingPoly (Z k))