Correctness of the effective coprime-degree composed-sum construction #
theorem
MIPRE.LowDegree.BinaryQuotient.root_frobenius_period
(f : Polynomial (ZMod 2))
(hf : f.Monic)
[Fact (Irreducible f)]
:
The canonical root's Frobenius orbit closes at the degree of its modulus.
theorem
MIPRE.LowDegree.BinaryQuotient.map_composedSumBits
(f : Polynomial (ZMod 2))
(hf : f.Monic)
[Fact (Irreducible f)]
(p g : Cost.BitStr)
(hp : List.length p = f.natDegree)
(hpoly : f = polyOfBits (p ++ [true]))
(hg : (polyOfBits g).Monic)
:
Polynomial.map (algebraMap (ZMod 2) (AdjoinRoot f)) (polyOfBits (composedSumBits p g)) = composedSumPolynomial (polyOfBits g) (AdjoinRoot.root f) f.natDegree
The executable composed-sum output has the specified product interpretation.
theorem
MIPRE.LowDegree.BinaryQuotient.composedSumBits_monic_natDegree
(f : Polynomial (ZMod 2))
(hf : f.Monic)
[Fact (Irreducible f)]
(p g : Cost.BitStr)
(hp : List.length p = f.natDegree)
(hpoly : f = polyOfBits (p ++ [true]))
(hg : (polyOfBits g).Monic)
:
(polyOfBits (composedSumBits p g)).Monic ∧ (polyOfBits (composedSumBits p g)).natDegree = f.natDegree * (polyOfBits g).natDegree
The descended composed sum is monic, of the product degree.
theorem
MIPRE.LowDegree.BinaryQuotient.composedSumBits_correct
(f : Polynomial (ZMod 2))
(hf : f.Monic)
[Fact (Irreducible f)]
(p g : Cost.BitStr)
(hp : List.length p = f.natDegree)
(hpoly : f = polyOfBits (p ++ [true]))
(hg : (polyOfBits g).Monic)
(hgi : Irreducible (polyOfBits g))
(hcop : f.natDegree.Coprime (polyOfBits g).natDegree)
:
(polyOfBits (composedSumBits p g)).Monic ∧ Irreducible (polyOfBits (composedSumBits p g)) ∧ (polyOfBits (composedSumBits p g)).natDegree = f.natDegree * (polyOfBits g).natDegree
The uniform composed-sum program combines irreducible polynomials of coprime degrees.