Correctness of the bounded odd-prime auxiliary construction

structure MIPRE.LowDegree.BinaryPolynomial.NonresidueInvariant (q m i : ℕ) (s : NonresidueState) : Prop

The executable loop's invariant, including the primitive-order progress counter.

• exponent : List.length s.1 + 1 = q
• cap : List.length s.2.1 = m + 1
• canonical : List.getLastD s.2.2.2 false = true
• irreducible : Irreducible (polyOfBits s.2.2.2)
• degree : (polyOfBits s.2.2.2).natDegree = m
• stopped : s.2.2.1 = true → ∀ (b : AdjoinRoot (polyOfBits s.2.2.2)), b ^ q ≠ AdjoinRoot.root (polyOfBits s.2.2.2)
• running : s.2.2.1 = false → polyOfBits s.2.2.2 ∣ Polynomial.cyclotomic (q ^ (i + 1)) (ZMod 2)

theorem MIPRE.LowDegree.BinaryPolynomial.liftCandidates_spec (q m i : ℕ) (s : NonresidueState) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hv : NonresidueInvariant q m i s) (hd : s.2.2.1 = false) : liftCandidates s ≠ [] ∧ (List.map polyOfBits (liftCandidates s)).prod = (polyOfBits s.2.2.2).comp (Polynomial.X ^ q) ∧ (∀ b ∈ liftCandidates s, List.getLastD b false = true ∧ (polyOfBits b).Monic ∧ Irreducible (polyOfBits b)) ∧ ((liftCandidates s).tail.isEmpty = true ↔ Irreducible ((polyOfBits s.2.2.2).comp (Polynomial.X ^ q)))

The exact specification of the factorization query made by a valid running state.

theorem MIPRE.LowDegree.BinaryPolynomial.liftCandidates_degree (q m i : ℕ) (s : NonresidueState) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hv : NonresidueInvariant q m i s) (hd : s.2.2.1 = false) (ht : (liftCandidates s).tail.isEmpty = false) (b : Cost.BitStr) : b ∈ liftCandidates s → (polyOfBits b).natDegree = m

On a nonterminal query, the selected factor has precisely the seed degree.

theorem MIPRE.LowDegree.BinaryPolynomial.nonresidueStep_invariant (q m i : ℕ) (s : NonresidueState) (b : Bool) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hv : NonresidueInvariant q m i s) : NonresidueInvariant q m (i + 1) (nonresidueStep s b)

Every executable step either certifies a nonresidue or advances primitive order.

theorem MIPRE.LowDegree.BinaryPolynomial.fold_nonresidueStep_invariant (l : Cost.BitStr) (q m i : ℕ) (s : NonresidueState) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hv : NonresidueInvariant q m i s) : NonresidueInvariant q m (i + List.length l) (List.foldl nonresidueStep s l)

The bounded loop preserves its invariant with one progress count per fuel bit.

theorem MIPRE.LowDegree.BinaryPolynomial.nonresidueInvariant_stopped (q m i : ℕ) (s : NonresidueState) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hv : NonresidueInvariant q m i s) (hi : m ≤ i) : s.2.2.1 = true

A valid state cannot still be running after the seed-degree budget is exhausted.

theorem MIPRE.LowDegree.BinaryPolynomial.cyclotomicSeedBits_canonical (q : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) : List.getLastD (cyclotomicSeedBits (Cost.unary q)) false = true

The initial seed uses exactly its degree plus one coefficients.

theorem MIPRE.LowDegree.BinaryPolynomial.nonresidueLiftStateProg_apply (u : Cost.Unary) : nonresidueLiftStateProg.toFun u = List.foldl nonresidueStep (List.tail u, Cost.unary (List.length (cyclotomicSeedBits u)), false, cyclotomicSeedBits u) (List.tail (cyclotomicSeedBits u))

Explicit execution of the seed-initialized auxiliary loop.

theorem MIPRE.LowDegree.BinaryPolynomial.nonresidueLiftBitsProg_correct (q : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) : have f := polyOfBits (nonresidueLiftBitsProg.toFun (Cost.unary q)); List.getLastD (nonresidueLiftBitsProg.toFun (Cost.unary q)) false = true ∧ f.Monic ∧ Irreducible f ∧ f.natDegree = (polyOfBits (cyclotomicSeedBits (Cost.unary q))).natDegree ∧ ∀ (b : AdjoinRoot f), b ^ q ≠ AdjoinRoot.root f

The polynomial-time auxiliary constructor returns a monic irreducible polynomial of the seed degree whose specified root is an odd-prime nonresidue.

theorem MIPRE.LowDegree.BinaryPolynomial.nonresidueLiftBits_order (q : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) : orderOf 2 = (polyOfBits (nonresidueLiftBitsProg.toFun (Cost.unary q))).natDegree

The auxiliary degree is exactly the multiplicative order of two modulo the prime.

theorem MIPRE.LowDegree.BinaryPolynomial.nonresidueLiftBits_degree_coprime (q : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) : q.Coprime (polyOfBits (nonresidueLiftBitsProg.toFun (Cost.unary q))).natDegree

The auxiliary degree is coprime to the requested odd prime.