The effective self-dual normal basis theorem

Starting only with the unary odd degree, the program constructs Shoup's quotient field, a normal element by fixed-space projections, its self-dualized Frobenius orbit, and all multiplication-table bits. No abstract choice of a normal element occurs in the program. The underlying Shoup constructor is proved by a specified polynomial-time program, and the construction uses only the standard Lean axioms.

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

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

Equations

• MIPRE.SAT.shoupSelfDualNormalBasis k hk hodd = MIPRE.SAT.shoupSelfDualBasis k hk hodd (MIPRE.SAT.shoupNormalBasis k hk hodd) ⋯

theorem MIPRE.SAT.shoupSelfDualNormalBasis_selfDual (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) : LowDegree.IsSelfDualBasis (shoupSelfDualNormalBasis k hk hodd)

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

noncomputable def MIPRE.SAT.shoupSelfDualNormalBasisProg : Cost.PolyTimeFun Cost.Unary (List Cost.BitStr)

The uniform unary-degree basis constructor.

Equations

• MIPRE.SAT.shoupSelfDualNormalBasisProg = MIPRE.SAT.shoupSelfDualizeProg.comp ((MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Unary).pair MIPRE.SAT.shoupNormalBasisProg)

theorem MIPRE.SAT.shoupSelfDualNormalBasisProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) : shoupSelfDualNormalBasisProg.toFun (Cost.unary k) = List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits ((shoupSelfDualNormalBasis k hk hodd) i)

noncomputable def MIPRE.SAT.shoupSelfDualNormalDataProg : Cost.PolyTimeFun Cost.Unary (List Cost.BitStr × List (List Cost.BitStr))

Basis vectors in the polynomial representation, followed by products in the new basis.

Equations

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

theorem MIPRE.SAT.shoupSelfDualNormalDataProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) : shoupSelfDualNormalDataProg.toFun (Cost.unary k) = (List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits ((shoupSelfDualNormalBasis k hk hodd) i), List.ofFn fun (i : Fin k) => List.ofFn fun (j : Fin k) => LowDegree.BinaryLinear.vectorBits ((shoupSelfDualNormalBasis k hk hodd).equivFun ((shoupSelfDualNormalBasis k hk hodd) i * (shoupSelfDualNormalBasis k hk hodd) j)))

theorem MIPRE.SAT.shoupSelfDualNormalDataProg_time_le : ∃ (R : Polynomial ℕ), ∀ (k : ℕ), ∃ t ≤ Polynomial.eval k R, shoupSelfDualNormalDataProg.code.Runs (Cost.encode (Cost.unary k)) (Cost.encode (shoupSelfDualNormalDataProg.toFun (Cost.unary k))) t

The complete construction, including all table entries, takes polynomial time in degree.

theorem MIPRE.SAT.effective_selfDualNormalBasis : ∃ (R : Polynomial ℕ), ∀ (k : ℕ) (hk : 1 ≤ k), Odd k → ∃ (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier), LowDegree.IsSelfDualBasis b ∧ LowDegree.IsNormalBasis b ∧ ∃ t ≤ Polynomial.eval k R, shoupSelfDualNormalDataProg.code.Runs (Cost.encode (Cost.unary k)) (Cost.encode (List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i), List.ofFn fun (i : Fin k) => List.ofFn fun (j : Fin k) => LowDegree.BinaryLinear.vectorBits (b.equivFun (b i * b j)))) t

The algorithmic self-dual normal basis theorem, with its exact ambient output and runtime.