Effective self-dualization of a supplied normal basis

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

noncomputable def MIPRE.SAT.shoupChangedVectors (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (H : Matrix (Fin k) (Fin k) (ZMod 2)) : Fin k → (shoupBinField k hk).carrier

Apply a binary matrix to the columns of a supplied field basis.

Equations

• MIPRE.SAT.shoupChangedVectors k hk b H i = ∑ j : Fin k, H j i • b j

theorem MIPRE.SAT.shoupChangedVectors_gram (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (H : Matrix (Fin k) (Fin k) (ZMod 2)) : shoupTraceGram k hk (shoupChangedVectors k hk b H) = H.transpose * shoupTraceGram k hk ⇑b * H

Basis changes transform the trace Gram matrix by the usual congruence.

theorem MIPRE.SAT.shoupTraceGram_one_linearIndependent (k : ℕ) (hk : 1 ≤ k) (v : Fin k → (shoupBinField k hk).carrier) (hv : shoupTraceGram k hk v = 1) : LinearIndependent (ZMod 2) v

An identity trace Gram matrix proves linear independence.

theorem MIPRE.SAT.shoupChangedVectors_normal (k : ℕ) (hk : 1 ≤ k) [NeZero k] (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (hb : LowDegree.IsNormalBasis b) (h : Fin k → ZMod 2) : ∃ (a : (shoupBinField k hk).carrier), ∀ (i : Fin k), shoupChangedVectors k hk b (Matrix.circulant h) i = a ^ 2 ^ ↑i

A circulant change of coordinates preserves the orbit form of a normal basis.

noncomputable def MIPRE.SAT.shoupSelfDualVectors (k : ℕ) (hk : 1 ≤ k) [NeZero k] (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) : Fin k → (shoupBinField k hk).carrier

The self-dualizing vectors computed from a supplied normal basis.

Equations

• MIPRE.SAT.shoupSelfDualVectors k hk b = MIPRE.SAT.shoupChangedVectors k hk b (MIPRE.LowDegree.BinaryLinear.inverseRootMatrix (MIPRE.SAT.shoupTraceGram k hk ⇑b))

theorem MIPRE.SAT.shoupSelfDualVectors_gram (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (hb : LowDegree.IsNormalBasis b) : shoupTraceGram k hk (shoupSelfDualVectors k hk b) = 1

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

Self-dualization gives an actual basis with exactly the computed vectors.

Equations

• MIPRE.SAT.shoupSelfDualBasis k hk hodd b hb = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

theorem MIPRE.SAT.shoupSelfDualBasis_apply (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (hb : LowDegree.IsNormalBasis b) (i : Fin k) : (shoupSelfDualBasis k hk hodd b hb) i = shoupSelfDualVectors k hk b i

theorem MIPRE.SAT.shoupSelfDualBasis_selfDual (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (hb : LowDegree.IsNormalBasis b) : LowDegree.IsSelfDualBasis (shoupSelfDualBasis k hk hodd b hb)

theorem MIPRE.SAT.shoupSelfDualBasis_normal (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (hb : LowDegree.IsNormalBasis b) : LowDegree.IsNormalBasis (shoupSelfDualBasis k hk hodd b hb)

theorem MIPRE.SAT.shoupChangedVectors_encoding (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (H : Matrix (Fin k) (Fin k) (ZMod 2)) (j : Fin k) : (shoupBinField k hk).toBits (shoupChangedVectors k hk b H j) = LowDegree.BinaryLinear.vectorBits ((shoupBasisMatrix k hk b * H).col j)

Polynomial-basis coordinates of the changed family are the matrix product columns.

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

Construct and apply the inverse Gram square root, returning the new basis vectors.

Equations

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

theorem MIPRE.SAT.shoupSelfDualizeProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (hb : LowDegree.IsNormalBasis b) : shoupSelfDualizeProg.toFun (Cost.unary k, List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i)) = List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits ((shoupSelfDualBasis k hk hodd b hb) i)

Every output vector is the canonical encoding of the constructed self-dual normal basis.

theorem MIPRE.SAT.shoupSelfDualizeProg_time_le : ∃ (R : Polynomial ℕ), ∀ (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier), ∃ t ≤ Polynomial.eval k R, shoupSelfDualizeProg.code.Runs (Cost.encode (Cost.unary k, List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i))) (Cost.encode (shoupSelfDualizeProg.toFun (Cost.unary k, List.ofFn fun (i : Fin k) => (shoupBinField k hk).toBits (b i)))) t

The complete change of basis, including its Gram inverse, has polynomial runtime.