Effective binary cyclic group algebra coordinates

theorem MIPRE.LowDegree.BinaryLinear.instFactPrimeOfNatNat_mIPRE_1 : Fact (Nat.Prime 2)

instance MIPRE.LowDegree.BinaryLinear.groupAlgebraCharP (k : ℕ) [NeZero k] : CharP (AddMonoidAlgebra (ZMod 2) (Fin k)) 2

noncomputable def MIPRE.LowDegree.BinaryLinear.groupCoordinates (k : ℕ) : AddMonoidAlgebra (ZMod 2) (Fin k) ≃ₗ[ZMod 2] Fin k → ZMod 2

All cyclic group-algebra coefficients as a binary linear equivalence.

Equations

• MIPRE.LowDegree.BinaryLinear.groupCoordinates k = (AddMonoidAlgebra.coeffLinearEquiv (ZMod 2)).trans (Finsupp.linearEquivFunOnFinite (ZMod 2) (ZMod 2) (Fin k))

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.groupCoordinates_apply (k : ℕ) (z : AddMonoidAlgebra (ZMod 2) (Fin k)) (i : Fin k) : (groupCoordinates k) z i = z.coeff i

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.groupCoordinates_finGroupOfVector {k : ℕ} [NeZero k] (v : Fin k → ZMod 2) : (groupCoordinates k) (finGroupOfVector v) = v

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.groupCoordinates_symm_apply {k : ℕ} [NeZero k] (v : Fin k → ZMod 2) : (groupCoordinates k).symm v = finGroupOfVector v

noncomputable def MIPRE.LowDegree.BinaryLinear.groupMulBitsProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr

Cyclic convolution, using the verified circulant printer and matrix application.

Equations

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

theorem MIPRE.LowDegree.BinaryLinear.groupMulBitsProg_correct {k : ℕ} [NeZero k] (z w : AddMonoidAlgebra (ZMod 2) (Fin k)) : groupMulBitsProg.toFun (vectorBits ((groupCoordinates k) z), vectorBits ((groupCoordinates k) w)) = vectorBits ((groupCoordinates k) (z * w))

noncomputable def MIPRE.LowDegree.BinaryLinear.groupSquareLinear (k : ℕ) [NeZero k] : AddMonoidAlgebra (ZMod 2) (Fin k) →ₗ[ZMod 2] AddMonoidAlgebra (ZMod 2) (Fin k)

Squaring in a binary commutative group algebra is a linear map.

Equations

• MIPRE.LowDegree.BinaryLinear.groupSquareLinear k = (FiniteField.frobeniusAlgHom (ZMod 2) (AddMonoidAlgebra (ZMod 2) (Fin k))).toLinearMap

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.groupSquareLinear_apply (k : ℕ) [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) : (groupSquareLinear k) z = z * z

noncomputable def MIPRE.LowDegree.BinaryLinear.groupSquareCoordinates (k : ℕ) [NeZero k] : (Fin k → ZMod 2) →ₗ[ZMod 2] Fin k → ZMod 2

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.groupSquareCoordinates_apply (k : ℕ) [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) : (groupSquareCoordinates k) ((groupCoordinates k) z) = (groupCoordinates k) (z * z)

noncomputable def MIPRE.LowDegree.BinaryLinear.groupSquareMatrix (k : ℕ) [NeZero k] : Matrix (Fin k) (Fin k) (ZMod 2)

Equations

• MIPRE.LowDegree.BinaryLinear.groupSquareMatrix k = LinearMap.toMatrix' (MIPRE.LowDegree.BinaryLinear.groupSquareCoordinates k)

noncomputable def MIPRE.LowDegree.BinaryLinear.groupSquareMatrixProg : Cost.PolyTimeFun Cost.Unary (List Cost.BitStr)

Print the squaring matrix by applying cyclic convolution to the coordinate units.

Equations

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

theorem MIPRE.LowDegree.BinaryLinear.groupSquareMatrixProg_correct (k : ℕ) [NeZero k] : groupSquareMatrixProg.toFun (Cost.unary k) = matrixBits (groupSquareMatrix k)

noncomputable def MIPRE.LowDegree.BinaryLinear.groupFixedMatrix (k : ℕ) [NeZero k] : Matrix (Fin k) (Fin k) (ZMod 2)

The fixed-space equation is squaring plus the identity, in characteristic two.

Equations

• MIPRE.LowDegree.BinaryLinear.groupFixedMatrix k = MIPRE.LowDegree.BinaryLinear.groupSquareMatrix k + 1

theorem MIPRE.LowDegree.BinaryLinear.groupFixedMatrix_ker (k : ℕ) [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) : (groupCoordinates k) z ∈ (groupFixedMatrix k).mulVecLin.ker ↔ z * z = z

noncomputable def MIPRE.LowDegree.BinaryLinear.groupFixedMatrixProg : Cost.PolyTimeFun Cost.Unary (List Cost.BitStr)

Construct the binary fixed-space equation.

Equations

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

theorem MIPRE.LowDegree.BinaryLinear.groupFixedMatrixProg_correct (k : ℕ) [NeZero k] : groupFixedMatrixProg.toFun (Cost.unary k) = matrixBits (groupFixedMatrix k)

noncomputable def MIPRE.LowDegree.BinaryLinear.groupFixedGeneratorsProg : Cost.PolyTimeFun Cost.Unary (List Cost.BitStr)

At most k coefficient vectors generate all idempotents of the binary cyclic algebra.

Equations

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

noncomputable def MIPRE.LowDegree.BinaryLinear.groupFixedGenerator (k : ℕ) [NeZero k] (j : Fin k) : AddMonoidAlgebra (ZMod 2) (Fin k)

Equations

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

theorem MIPRE.LowDegree.BinaryLinear.groupFixedGenerator_idempotent (k : ℕ) [NeZero k] (j : Fin k) : groupFixedGenerator k j * groupFixedGenerator k j = groupFixedGenerator k j

theorem MIPRE.LowDegree.BinaryLinear.groupFixedGenerator_spans (k : ℕ) [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) (hz : z * z = z) : z ∈ Submodule.span (ZMod 2) (Set.range (groupFixedGenerator k))

Every idempotent lies in the binary span of the computed generators.

theorem MIPRE.LowDegree.BinaryLinear.groupFixedGeneratorsProg_correct (k : ℕ) [NeZero k] : groupFixedGeneratorsProg.toFun (Cost.unary k) = List.ofFn fun (j : Fin k) => vectorBits ((groupCoordinates k) (groupFixedGenerator k j))

Exact encoding of the computed fixed-space generators; no linear combinations are enumerated.