Uniform polynomial-time remainder by binary polynomials

One deterministic polynomial-time evaluator computes the remainder of two runtime coefficient lists, including padded and zero moduli. The proof uses a bounded maximum to find the modulus width and a bounded high-to-low fold for long division. The registered certificates support automatic composition with later encoded polynomial and finite-field programs.

theorem Complexity.BitPolynomial.significantLength_unary : UnaryFn significantLength

The significant coefficient width is computable in unary in polynomial time.

theorem Complexity.BitPolynomial.remainderEval_mem_FP : remainderEval ∈ FP

Remainder by a runtime binary modulus is uniformly polynomial-time.