Computing Frobenius matrices in arbitrary monic binary quotients

theorem MIPRE.LowDegree.BinaryQuotient.toBits_eq_vectorBits (f : Polynomial (ZMod 2)) (hf : f.Monic) (x : AdjoinRoot f) : toBits f hf x = BinaryLinear.vectorBits ((coordinateEquiv f hf) x)

Quotient bit encodings agree with the generic binary linear coordinates.

theorem MIPRE.LowDegree.BinaryQuotient.toBits_basis (f : Polynomial (ZMod 2)) (hf : f.Monic) (j : Fin f.natDegree) : toBits f hf ((AdjoinRoot.powerBasisAux' hf) j) = BinaryLinear.unitBits f.natDegree ↑j

A power-basis vector has the corresponding standard unit-vector encoding.

noncomputable def MIPRE.LowDegree.BinaryQuotient.frobeniusLinear (f : Polynomial (ZMod 2)) : AdjoinRoot f →ₗ[ZMod 2] AdjoinRoot f

Frobenius is binary linear even when the quotient is not a field.

Equations

• MIPRE.LowDegree.BinaryQuotient.frobeniusLinear f = (FiniteField.frobeniusAlgHom (ZMod 2) (AdjoinRoot f)).toLinearMap

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.frobeniusLinear_apply (f : Polynomial (ZMod 2)) (x : AdjoinRoot f) : (frobeniusLinear f) x = x ^ 2

In a binary algebra the Frobenius map is squaring.

noncomputable def MIPRE.LowDegree.BinaryQuotient.frobeniusMatrix (f : Polynomial (ZMod 2)) (hf : f.Monic) : Matrix (Fin f.natDegree) (Fin f.natDegree) (ZMod 2)

Frobenius in the specified monic power basis.

Equations

• MIPRE.LowDegree.BinaryQuotient.frobeniusMatrix f hf = (LinearMap.toMatrix (AdjoinRoot.powerBasisAux' hf) (AdjoinRoot.powerBasisAux' hf)) (MIPRE.LowDegree.BinaryQuotient.frobeniusLinear f)

noncomputable def MIPRE.LowDegree.BinaryQuotient.squareProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr

Squaring modulo a supplied monic polynomial, without constructing a field.

Equations

• MIPRE.LowDegree.BinaryQuotient.squareProg = MIPRE.LowDegree.BinaryPolynomial.mulReduceProg.comp (MIPRE.Cost.PolyTimeFun.fst.pair (MIPRE.Cost.PolyTimeFun.snd.pair MIPRE.Cost.PolyTimeFun.snd))

theorem MIPRE.LowDegree.BinaryQuotient.squareProg_correct (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (x : AdjoinRoot f) : squareProg.toFun (p, toBits f hf x) = toBits f hf ((frobeniusLinear f) x)

The supplied-modulus squaring program prints the canonical quotient encoding.

noncomputable def MIPRE.LowDegree.BinaryQuotient.frobeniusMatrixProg : Cost.PolyTimeFun Cost.BitStr (List Cost.BitStr)

Compute the squares of the power-basis vectors and transpose their columns.

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.frobeniusMatrixProg_correct (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) : frobeniusMatrixProg.toFun p = BinaryLinear.matrixBits (frobeniusMatrix f hf)

The ambient program computes the exact Frobenius matrix of a monic quotient. Its columns encode the squares of 1,X,...,X^(d-1), not repeated squarings of X.

noncomputable def MIPRE.LowDegree.BinaryQuotient.fixedMatrix (f : Polynomial (ZMod 2)) (hf : f.Monic) : Matrix (Fin f.natDegree) (Fin f.natDegree) (ZMod 2)

The fixed-space equation for quotient Frobenius.

Equations

• MIPRE.LowDegree.BinaryQuotient.fixedMatrix f hf = MIPRE.LowDegree.BinaryQuotient.frobeniusMatrix f hf + 1

theorem MIPRE.LowDegree.BinaryQuotient.fixedMatrix_ker (f : Polynomial (ZMod 2)) (hf : f.Monic) (x : AdjoinRoot f) : (coordinateEquiv f hf) x ∈ (fixedMatrix f hf).mulVecLin.ker ↔ x * x = x

The binary matrix kernel is exactly the set of quotient idempotents.

noncomputable def MIPRE.LowDegree.BinaryQuotient.fixedMatrixProg : Cost.PolyTimeFun Cost.BitStr (List Cost.BitStr)

Compute Frobenius plus identity on coefficient vectors.

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.fixedMatrixProg_correct (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) : fixedMatrixProg.toFun p = BinaryLinear.matrixBits (fixedMatrix f hf)

The fixed-space equation is generated uniformly from the supplied modulus.

noncomputable def MIPRE.LowDegree.BinaryQuotient.fixedGeneratorsProg : Cost.PolyTimeFun Cost.BitStr (List Cost.BitStr)

Print a bounded family spanning the quotient's complete Frobenius fixed space.

Equations

• MIPRE.LowDegree.BinaryQuotient.fixedGeneratorsProg = MIPRE.LowDegree.BinaryLinear.kernelGeneratorsProg.comp (MIPRE.Cost.PolyTimeFun.length.pair MIPRE.LowDegree.BinaryQuotient.fixedMatrixProg)

noncomputable def MIPRE.LowDegree.BinaryQuotient.fixedGenerator (f : Polynomial (ZMod 2)) (hf : f.Monic) (j : Fin f.natDegree) : AdjoinRoot f

Abstract interpretation of the computed kernel generators in the quotient.

Equations

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

theorem MIPRE.LowDegree.BinaryQuotient.fixedGenerator_idempotent (f : Polynomial (ZMod 2)) (hf : f.Monic) (j : Fin f.natDegree) : fixedGenerator f hf j * fixedGenerator f hf j = fixedGenerator f hf j

Every generated quotient element is idempotent.

theorem MIPRE.LowDegree.BinaryQuotient.fixedGenerator_spans (f : Polynomial (ZMod 2)) (hf : f.Monic) (x : AdjoinRoot f) (hx : x * x = x) : x ∈ Submodule.span (ZMod 2) (Set.range (fixedGenerator f hf))

All idempotents lie in the binary span of the computed generator family.

theorem MIPRE.LowDegree.BinaryQuotient.fixedGeneratorsProg_correct (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) : fixedGeneratorsProg.toFun p = List.ofFn fun (j : Fin f.natDegree) => toBits f hf (fixedGenerator f hf j)

The program prints exactly the canonical coordinates of these generators.