Correct binary-polynomial remainder with a runtime modulus

ofBits_remainderBits identifies the concrete list algorithm with polynomial remainder over ZMod 2 for every dividend and modulus. High zero padding does not change the modulus. A zero modulus returns the original dividend, while a constant-one modulus produces the empty coefficient list.

The high-to-low scan stores exactly the modulus degree in bits. Its width is bounded by the supplied modulus length, and the total evaluator's output is bounded by the larger input length. The uniform polynomial-time certificate is in Complexitylib.Classes.P.BitPolynomial.Remainder.

theorem Complexity.BitPolynomial.significantLength_le (bits : List Bool) : significantLength bits ≤ bits.length

The significant coefficient width never exceeds the input length.

theorem Complexity.BitPolynomial.significantLength_eq_zero_iff (bits : List Bool) : significantLength bits = 0 ↔ ofBits bits = 0

Significant width zero means exactly that all represented coefficients are zero.

theorem Complexity.BitPolynomial.ofBits_natDegree (bits : List Bool) (nonzero : ofBits bits ≠ 0) : (ofBits bits).natDegree = significantLength bits - 1

For a nonzero polynomial, significant width is one past its degree.

theorem Complexity.BitPolynomial.remainderStep_length (modulus : List Bool) (bit : Bool) (state : List Bool) : (remainderStep modulus bit state).length = significantLength modulus - 1

Every cancellation step restores the fixed width, including width zero.

theorem Complexity.BitPolynomial.remainderScan_length (modulus a : List Bool) : (remainderScan modulus a).length = significantLength modulus - 1

Every intermediate scan state has the fixed remainder width.

theorem Complexity.BitPolynomial.remainderBits_length (a modulus : List Bool) : (remainderBits a modulus).length = if significantLength modulus = 0 then a.length else significantLength modulus - 1

Exact output length, with the unchanged-dividend convention for a zero modulus.

theorem Complexity.BitPolynomial.remainderBits_length_le (a modulus : List Bool) : (remainderBits a modulus).length ≤ max a.length modulus.length

The output length is bounded by the larger operand length.

theorem Complexity.BitPolynomial.ofBits_remainderBits (a modulus : List Bool) : ofBits (remainderBits a modulus) = ofBits a %ₘ ofBits modulus

The total bit-list algorithm computes polynomial remainder for every modulus.

theorem Complexity.BitPolynomial.remainderEval_pair (a modulus : List Bool) : remainderEval (pair a modulus) = remainderBits a modulus

The evaluator reads its dividend and modulus from the standard pairing codec.