Deterministic squarefree factorization over the binary field

Frobenius fixed-space separation computes primitive idempotents of the monic quotient. The factor supported by an idempotent represented by E is gcd(f, E - 1). All executing operations are uniform ambient programs; the finite-ring arguments justify correctness without enumerating the quotient.

theorem MIPRE.LowDegree.BinaryQuotient.polyOfBits_xorBits (a b : Cost.BitStr) (h : List.length a = List.length b) : polyOfBits (BinaryPolynomial.xorBits a b) = polyOfBits a + polyOfBits b

XOR is binary polynomial addition on equal-width lists.

theorem MIPRE.LowDegree.BinaryQuotient.polyOfBits_oneBits (p : Cost.BitStr) (hp : p ≠ []) : polyOfBits (BinaryPolynomial.oneBits p) = 1

Fixed-width one represents the constant polynomial one at every positive width.

noncomputable def MIPRE.LowDegree.BinaryQuotient.factorBits (p : Cost.BitStr) : List Cost.BitStr

The factor list extracted from the computed primitive components.

Equations

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

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

Equations

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

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

A fixed deterministic polynomial-time squarefree binary factorization program. Its input consists of the lower coefficients of the monic polynomial.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.factorBitsProg_apply (p : Cost.BitStr) : factorBitsProg.toFun p = factorBits p

theorem MIPRE.LowDegree.BinaryQuotient.factorBitsProg_polynomials (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (hp0 : p ≠ []) : List.map polyOfBits (factorBitsProg.toFun p) = List.map (fun (e : AdjoinRoot f) => componentFactor f (polyOfBits (toBits f hf e))) (components f hf)

The extracted coefficient lists represent precisely the primitive-component factors.

theorem MIPRE.LowDegree.BinaryQuotient.factorBitsProg_factors (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (hp0 : p ≠ []) (hs : Squarefree f) (a : Cost.BitStr) : a ∈ factorBitsProg.toFun p → (polyOfBits a).Monic ∧ Irreducible (polyOfBits a)

Every output of squarefree binary factorization is monic and irreducible.

theorem MIPRE.LowDegree.BinaryQuotient.factorBitsProg_prod (f : Polynomial (ZMod 2)) (hf : f.Monic) (p : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (hp0 : p ≠ []) (hs : Squarefree f) : (List.map polyOfBits (factorBitsProg.toFun p)).prod = f

The output factors reconstruct the entire input polynomial.