A normal element from primitive Frobenius projections

theorem MIPRE.SAT.instFactPrimeOfNatNat_mIPRE_5 : Fact (Nat.Prime 2)

def MIPRE.SAT.firstNonzero {E : Type u_1} [Zero E] [DecidableEq E] : List E → E

Deterministically select the first nonzero element, with zero as the empty default.

Equations

• MIPRE.SAT.firstNonzero [] = 0
• MIPRE.SAT.firstNonzero (a :: l) = if a = 0 then MIPRE.SAT.firstNonzero l else a

theorem MIPRE.SAT.firstNonzero_eq_zero_iff {E : Type u_1} [Zero E] [DecidableEq E] (l : List E) : firstNonzero l = 0 ↔ ∀ a ∈ l, a = 0

theorem MIPRE.SAT.firstNonzero_property {E : Type u_1} [Zero E] [DecidableEq E] (P : E → Prop) (hzero : P 0) (l : List E) (hl : ∀ a ∈ l, P a) : P (firstNonzero l)

noncomputable def MIPRE.SAT.shoupProjectedVector (k : ℕ) (hk : 1 ≤ k) [NeZero k] (e : AddMonoidAlgebra (ZMod 2) (Fin k)) : (shoupBinField k hk).carrier

Scan the polynomial basis for the first nonzero image of a cyclic operator.

Equations

• MIPRE.SAT.shoupProjectedVector k hk e = MIPRE.SAT.firstNonzero (List.ofFn fun (j : Fin k) => ((MIPRE.SAT.shoupFrobeniusAction k hk) e) ((MIPRE.SAT.shoupPowerBasis k hk) j))

theorem MIPRE.SAT.shoupProjectedVector_ne_zero (k : ℕ) (hk : 1 ≤ k) [NeZero k] (e : AddMonoidAlgebra (ZMod 2) (Fin k)) (he : e ≠ 0) : shoupProjectedVector k hk e ≠ 0

theorem MIPRE.SAT.shoupProjectedVector_supported (k : ℕ) (hk : 1 ≤ k) [NeZero k] (e : AddMonoidAlgebra (ZMod 2) (Fin k)) (he : e * e = e) : ((shoupFrobeniusAction k hk) e) (shoupProjectedVector k hk e) = shoupProjectedVector k hk e

noncomputable def MIPRE.SAT.shoupNormalElement (k : ℕ) (hk : 1 ≤ k) [NeZero k] : (shoupBinField k hk).carrier

Sum the selected nonzero projected vectors, in the computed component order.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.SAT.shoupNormalElement_projection (k : ℕ) (hk : 1 ≤ k) [NeZero k] (j : Fin (LowDegree.BinaryLinear.groupComponents k).length) : ((shoupFrobeniusAction k hk) ((LowDegree.BinaryLinear.groupComponents k).get j)) (shoupNormalElement k hk) = shoupProjectedVector k hk ((LowDegree.BinaryLinear.groupComponents k).get j)

noncomputable def MIPRE.SAT.shoupNormalOrbitMap (k : ℕ) (hk : 1 ≤ k) [NeZero k] : AddMonoidAlgebra (ZMod 2) (Fin k) →ₗ[ZMod 2] (shoupBinField k hk).carrier

Evaluation at the constructed element is a linear map from the cyclic algebra.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.SAT.shoupNormalOrbitMap_injective (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) : Function.Injective ⇑(shoupNormalOrbitMap k hk)

No nonzero cyclic operator kills the sum: each primitive component has its own nonzero image.

theorem MIPRE.SAT.shoupNormalElement_linearIndependent (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) : LinearIndependent (ZMod 2) fun (i : Fin k) => shoupNormalElement k hk ^ 2 ^ ↑i

The orbit of the computed normal element is linearly independent.

noncomputable def MIPRE.SAT.shoupNormalBasis (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier

The explicitly constructed Frobenius orbit as a basis.

Equations

• MIPRE.SAT.shoupNormalBasis k hk hodd = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

@[simp]

theorem MIPRE.SAT.shoupNormalBasis_apply (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (i : Fin k) : (shoupNormalBasis k hk hodd) i = shoupNormalElement k hk ^ 2 ^ ↑i

theorem MIPRE.SAT.shoupNormalBasis_normal (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) : LowDegree.IsNormalBasis (shoupNormalBasis k hk hodd)