Certified polynomial-time irreducibles of every odd-prime-power degree

theorem MIPRE.LowDegree.BinaryPolynomial.oddPrimePowerBits_width_le (q r : Cost.Unary) : List.length (oddPrimePowerBits q r) ≤ List.length r + 1

The output width is bounded by the requested degree even on malformed inputs.

theorem MIPRE.LowDegree.BinaryPolynomial.oddTraceBits_natDegree (q e : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) : have f := polyOfBits (nonresidueLiftBitsProg.toFun (Cost.unary q)); have F := f.comp (Polynomial.X ^ q ^ (e + 1)); (minpoly (ZMod 2) (evalBits (AdjoinRoot.root F) (oddTraceBits (Cost.unary q) (Cost.unary (q ^ (e + 1)))))).natDegree = q ^ (e + 1)

The trace generator in the explicit extension has exactly the requested odd-prime-power degree.

theorem MIPRE.LowDegree.BinaryPolynomial.oddPrimePowerBits_correct (q e : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) : have a := oddPrimePowerBits (Cost.unary q) (Cost.unary (q ^ (e + 1))); List.getLastD a false = true ∧ (polyOfBits a).Monic ∧ Irreducible (polyOfBits a) ∧ (polyOfBits a).natDegree = q ^ (e + 1)

The requested odd-prime-power constructor is correct, including canonical coefficient output.

theorem MIPRE.LowDegree.BinaryPolynomial.oddPrimePowerBits_length (q e : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) : List.length (oddPrimePowerBits (Cost.unary q) (Cost.unary (q ^ (e + 1)))) = q ^ (e + 1) + 1

The printed coefficient list has exactly degree plus one entries.