A globally bounded assembly of coprime prime-power irreducibles

def MIPRE.LowDegree.BinaryPolynomial.composedLowerBits (p g : Cost.BitStr) : Cost.BitStr

Lower coefficients of the normalized composed-sum polynomial.

Equations

• MIPRE.LowDegree.BinaryPolynomial.composedLowerBits p g = List.dropLast (MIPRE.LowDegree.BinaryPolynomial.normalizeBits (MIPRE.LowDegree.BinaryQuotient.composedSumBits p g))

theorem MIPRE.LowDegree.BinaryPolynomial.composedLowerBits_correct (p g : Cost.BitStr) (hp : Irreducible (polyOfBits (p ++ [true]))) (hg : (polyOfBits g).Monic) (hgi : Irreducible (polyOfBits g)) (hcop : (List.length p).Coprime (polyOfBits g).natDegree) : Irreducible (polyOfBits (composedLowerBits p g ++ [true])) ∧ List.length (composedLowerBits p g) = List.length p * (polyOfBits g).natDegree

The composed-sum lower coefficients preserve irreducibility and multiply degrees.

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryPolynomial.AssemblyState : Type

The unary target-degree cap and the current monic lower coefficients.

Equations

• MIPRE.LowDegree.BinaryPolynomial.AssemblyState = (MIPRE.Cost.Unary × MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryPolynomial.assemblyStep (s : AssemblyState) (g : Cost.BitStr) : AssemblyState

Every step clips its new modulus to the original unary target-degree cap.

Equations

• MIPRE.LowDegree.BinaryPolynomial.assemblyStep s g = (s.1, List.take (List.length s.1) (MIPRE.LowDegree.BinaryPolynomial.composedLowerBits s.2 g))

theorem MIPRE.LowDegree.BinaryPolynomial.assemblyStep_correct (u : Cost.Unary) (p g : Cost.BitStr) (hp : Irreducible (polyOfBits (p ++ [true]))) (hg : (polyOfBits g).Monic) (hgi : Irreducible (polyOfBits g)) (hcop : (List.length p).Coprime (polyOfBits g).natDegree) (hcap : List.length p * (polyOfBits g).natDegree ≤ List.length u) : Irreducible (polyOfBits ((assemblyStep (u, p) g).2 ++ [true])) ∧ List.length (assemblyStep (u, p) g).2 = List.length p * (polyOfBits g).natDegree

The cap is inert whenever the intended next degree is within the target.

theorem MIPRE.LowDegree.BinaryPolynomial.fold_assemblyStep_shape (l : List Cost.BitStr) (s : AssemblyState) : (List.foldl assemblyStep s l).1 = s.1 ∧ List.length (List.foldl assemblyStep s l).2 ≤ max (List.length s.2) (List.length s.1)

No raw fold state can exceed its initial width or the supplied cap.

theorem MIPRE.LowDegree.BinaryPolynomial.degree_prod_pos (l : List Cost.BitStr) (h : ∀ g ∈ l, Irreducible (polyOfBits g)) : 0 < (List.map (fun (g : List Bool) => (polyOfBits g).natDegree) l).prod

theorem MIPRE.LowDegree.BinaryPolynomial.fold_assemblyStep_correct (l : List Cost.BitStr) (u : Cost.Unary) (p : Cost.BitStr) (hp : Irreducible (polyOfBits (p ++ [true]))) (hl : ∀ g ∈ l, (polyOfBits g).Monic ∧ Irreducible (polyOfBits g)) (hpair : List.Pairwise (fun (g h : List Bool) => (polyOfBits g).natDegree.Coprime (polyOfBits h).natDegree) l) (hcop : ∀ g ∈ l, (List.length p).Coprime (polyOfBits g).natDegree) (hcap : List.length p * (List.map (fun (g : List Bool) => (polyOfBits g).natDegree) l).prod ≤ List.length u) : Irreducible (polyOfBits ((List.foldl assemblyStep (u, p) l).2 ++ [true])) ∧ List.length (List.foldl assemblyStep (u, p) l).2 = List.length p * (List.map (fun (g : List Bool) => (polyOfBits g).natDegree) l).prod

The bounded fold multiplies any pairwise coprime list of certified degrees.

noncomputable def MIPRE.LowDegree.BinaryPolynomial.assemblyStepProg : Cost.PolyTimeFun (AssemblyState × Cost.BitStr) AssemblyState

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.assemblyStepProg_apply (s : AssemblyState) (g : Cost.BitStr) : assemblyStepProg.toFun (s, g) = assemblyStep s g

theorem MIPRE.LowDegree.BinaryPolynomial.assemblyStep_bounded : assemblyStepProg.FoldBounded (5 * Polynomial.X + 5)

noncomputable def MIPRE.LowDegree.BinaryPolynomial.assembleBitsProg : Cost.PolyTimeFun (List Cost.BitStr × Cost.Unary × Cost.BitStr) Cost.BitStr

One uniform program assembles the supplied polynomial list with a global width cap.

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.assembleBitsProg_apply (l : List Cost.BitStr) (u : Cost.Unary) (p : Cost.BitStr) : assembleBitsProg.toFun (l, u, p) = (List.foldl assemblyStep (u, p) l).2

The bounded assembly program executes the specified fold.