Descending a closed orbit product to binary coefficient bits

theorem MIPRE.LowDegree.BinaryQuotient.coeff_coeffPolynomial {R : Type u_1} [CommRing R] (z : R) (cs : List Cost.BitStr) (i : ℕ) : (coeffPolynomial z cs).coeff i = BinaryPolynomial.evalBits z (cs.getD i [])

Coefficients of the interpreted nested list are the decoded list entries.

def MIPRE.LowDegree.BinaryQuotient.descendBits (cs : List Cost.BitStr) : Cost.BitStr

Select the constant coordinate of each quotient coefficient.

Equations

• MIPRE.LowDegree.BinaryQuotient.descendBits cs = List.map (fun (c : MIPRE.Cost.BitStr) => List.headD c false) cs

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

Coefficient descent has a fixed linear-time list program.

Equations

• MIPRE.LowDegree.BinaryQuotient.descendBitsProg = (MIPRE.Cost.PolyTimeFun.headD false).map

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.descendBitsProg_apply (cs : List Cost.BitStr) : descendBitsProg.toFun cs = descendBits cs

theorem MIPRE.LowDegree.BinaryQuotient.map_polyOfBits_descendBits {R : Type u_1} [CommRing R] [Algebra (ZMod 2) R] (z : R) (cs : List Cost.BitStr) (hc : ∀ c ∈ cs, BinaryPolynomial.evalBits z c = ofBool (List.headD c false)) : Polynomial.map (algebraMap (ZMod 2) R) (polyOfBits (descendBits cs)) = coeffPolynomial z cs

If every coefficient is its constant coordinate, descent recovers the same polynomial.

theorem MIPRE.LowDegree.BinaryQuotient.evalBits_eq_head_of_zero_or_one (f : Polynomial (ZMod 2)) (hf : f.Monic) (p c : Cost.BitStr) (hp : List.length p = f.natDegree) (hc : List.length c = f.natDegree) (hp0 : p ≠ []) (h : BinaryPolynomial.evalBits (AdjoinRoot.root f) c = 0 ∨ BinaryPolynomial.evalBits (AdjoinRoot.root f) c = 1) : BinaryPolynomial.evalBits (AdjoinRoot.root f) c = ofBool (List.headD c false)

In faithful fixed-width quotient coordinates, a zero or one has only its constant bit.

def MIPRE.LowDegree.BinaryQuotient.orbitPolynomialBits (u : Cost.Unary) (p a : Cost.BitStr) : Cost.BitStr

Print binary coefficients of the supplied Frobenius orbit.

Equations

• MIPRE.LowDegree.BinaryQuotient.orbitPolynomialBits u p a = MIPRE.LowDegree.BinaryQuotient.descendBits (MIPRE.LowDegree.BinaryQuotient.orbitProductBits u p a)

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

A uniform polynomial-time program for a binary orbit polynomial.

Equations

• MIPRE.LowDegree.BinaryQuotient.orbitPolynomialBitsProg = MIPRE.LowDegree.BinaryQuotient.descendBitsProg.comp MIPRE.LowDegree.BinaryQuotient.orbitProductBitsProg

@[simp]

theorem MIPRE.LowDegree.BinaryQuotient.orbitPolynomialBitsProg_apply (u : Cost.Unary) (p a : Cost.BitStr) : orbitPolynomialBitsProg.toFun (u, p, a) = orbitPolynomialBits u p a

theorem MIPRE.LowDegree.BinaryQuotient.map_orbitPolynomialBits (f : Polynomial (ZMod 2)) (hf : f.Monic) [Fact (Irreducible f)] (u : Cost.Unary) (p a : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (hp0 : p ≠ []) (ha : List.length a = List.length p) (hclosed : BinaryPolynomial.evalBits (AdjoinRoot.root f) a ^ 2 ^ List.length u = BinaryPolynomial.evalBits (AdjoinRoot.root f) a) : Polynomial.map (algebraMap (ZMod 2) (AdjoinRoot f)) (polyOfBits (orbitPolynomialBits u p a)) = orbitPolynomial (BinaryPolynomial.evalBits (AdjoinRoot.root f) a) (List.length u)

Closing an orbit in an irreducible quotient justifies executable coefficient descent.

theorem MIPRE.LowDegree.BinaryQuotient.orbitPolynomialBits_monic_natDegree (f : Polynomial (ZMod 2)) (hf : f.Monic) [Fact (Irreducible f)] (u : Cost.Unary) (p a : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (hp0 : p ≠ []) (ha : List.length a = List.length p) (hclosed : BinaryPolynomial.evalBits (AdjoinRoot.root f) a ^ 2 ^ List.length u = BinaryPolynomial.evalBits (AdjoinRoot.root f) a) : (polyOfBits (orbitPolynomialBits u p a)).Monic ∧ (polyOfBits (orbitPolynomialBits u p a)).natDegree = List.length u

The descended orbit product is monic and has the requested orbit degree.

theorem MIPRE.LowDegree.BinaryQuotient.orbitPolynomialBits_eq_minpoly (f : Polynomial (ZMod 2)) (hf : f.Monic) [Fact (Irreducible f)] (u : Cost.Unary) (p a : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (hp0 : p ≠ []) (ha : List.length a = List.length p) (hclosed : BinaryPolynomial.evalBits (AdjoinRoot.root f) a ^ 2 ^ List.length u = BinaryPolynomial.evalBits (AdjoinRoot.root f) a) (hu : 0 < List.length u) (hdegree : (minpoly (ZMod 2) (BinaryPolynomial.evalBits (AdjoinRoot.root f) a)).natDegree = List.length u) : polyOfBits (orbitPolynomialBits u p a) = minpoly (ZMod 2) (BinaryPolynomial.evalBits (AdjoinRoot.root f) a)

When the orbit length is the element's exact degree, the program prints its minimal polynomial.

theorem MIPRE.LowDegree.BinaryQuotient.orbitPolynomialBits_irreducible (f : Polynomial (ZMod 2)) (hf : f.Monic) [Fact (Irreducible f)] (u : Cost.Unary) (p a : Cost.BitStr) (hp : List.length p = f.natDegree) (hpoly : f = polyOfBits (p ++ [true])) (hp0 : p ≠ []) (ha : List.length a = List.length p) (hclosed : BinaryPolynomial.evalBits (AdjoinRoot.root f) a ^ 2 ^ List.length u = BinaryPolynomial.evalBits (AdjoinRoot.root f) a) (hu : 0 < List.length u) (hdegree : (minpoly (ZMod 2) (BinaryPolynomial.evalBits (AdjoinRoot.root f) a)).natDegree = List.length u) : Irreducible (polyOfBits (orbitPolynomialBits u p a))

The exact-degree orbit constructor produces an irreducible binary polynomial.