Canonical factor outputs and the executable irreducibility test

theorem MIPRE.LowDegree.BinaryQuotient.factorBitsProg_canonical (p a : Cost.BitStr) : a ∈ factorBitsProg.toFun p → a = [] ∨ List.getLastD a false = true

Every printed factor uses a canonical coefficient representation.

theorem MIPRE.LowDegree.BinaryQuotient.factor_dropLast_prod (a : Cost.BitStr) (ha : List.getLastD a false = true) (hp : 0 < (polyOfBits a).natDegree) (hs : Squarefree (polyOfBits a)) : (List.map polyOfBits (factorBitsProg.toFun (List.dropLast a))).prod = polyOfBits a

Factorization of a canonical full polynomial reconstructs it.

theorem MIPRE.LowDegree.BinaryQuotient.factor_dropLast_factors (a : Cost.BitStr) (ha : List.getLastD a false = true) (hp : 0 < (polyOfBits a).natDegree) (hs : Squarefree (polyOfBits a)) (b : Cost.BitStr) : b ∈ factorBitsProg.toFun (List.dropLast a) → List.getLastD b false = true ∧ (polyOfBits b).Monic ∧ Irreducible (polyOfBits b)

Every factor of a positive-degree squarefree canonical polynomial is irreducible.

theorem MIPRE.LowDegree.BinaryQuotient.factor_dropLast_ne_nil (a : Cost.BitStr) (ha : List.getLastD a false = true) (hp : 0 < (polyOfBits a).natDegree) (hs : Squarefree (polyOfBits a)) : factorBitsProg.toFun (List.dropLast a) ≠ []

Positive-degree inputs always produce at least one factor.

theorem MIPRE.LowDegree.BinaryQuotient.factor_dropLast_tail_isEmpty_iff (a : Cost.BitStr) (ha : List.getLastD a false = true) (hp : 0 < (polyOfBits a).natDegree) (hs : Squarefree (polyOfBits a)) : (factorBitsProg.toFun (List.dropLast a)).tail.isEmpty = true ↔ Irreducible (polyOfBits a)

The list stopping test is exactly irreducibility on valid factorization inputs.