Uniform polynomial-time binary remainder

A bounded maximum finds the modulus's significant length. Each long-division step reads and combines individual bits, and a bounded fold runs those steps from high coefficients to low coefficients. Every state has at most the modulus's input length, including the degree-zero case.

theorem Complexity.BitPolynomial.Internal.significantLength_unary : UnaryFn significantLength

theorem Complexity.BitPolynomial.Internal.remainderEval_mem_FP : remainderEval ∈ FP