Correct bounded binary modular Frobenius

For every nonzero runtime modulus, frobeniusBits a modulus count represents ofBits a ^ (2 ^ count.length) %ₘ ofBits modulus. Its state always has exactly significantLength modulus - 1 bits, independently of the exponent. This includes high zero padding, empty dividends, and constant-one moduli.

For a zero modulus the result is explicitly empty. The nested pairing pair (pair a modulus) count supplies all three runtime inputs. Malformed inputs follow the total pairing projections and the same guarded algorithm. The uniform FP certificate is in Complexitylib.Classes.P.BitPolynomial.Frobenius.

theorem Complexity.BitPolynomial.frobeniusStep_length (modulus state : List Bool) : (frobeniusStep modulus state).length = significantLength modulus - 1

Every guarded square-and-remainder step has the modulus's fixed degree width.

theorem Complexity.BitPolynomial.frobeniusBits_length (a modulus count : List Bool) : (frobeniusBits a modulus count).length = significantLength modulus - 1

Every state of the count-list fold has the modulus's fixed degree width.

theorem Complexity.BitPolynomial.frobeniusBits_length_le (a modulus count : List Bool) : (frobeniusBits a modulus count).length ≤ modulus.length

Output length is bounded by the supplied modulus length for all inputs.

theorem Complexity.BitPolynomial.frobeniusBits_of_modulus_zero (a modulus count : List Bool) (zero : ofBits modulus = 0) : frobeniusBits a modulus count = []

A zero modulus produces the empty list, independently of the dividend or count.

theorem Complexity.BitPolynomial.ofBits_frobeniusStep (modulus state : List Bool) (nonzero : ofBits modulus ≠ 0) : ofBits (frobeniusStep modulus state) = ofBits state ^ 2 %ₘ ofBits modulus

A guarded step computes one modular square whenever the modulus is nonzero.

theorem Complexity.BitPolynomial.ofBits_frobeniusBits (a modulus count : List Bool) (nonzero : ofBits modulus ≠ 0) : ofBits (frobeniusBits a modulus count) = ofBits a ^ 2 ^ count.length %ₘ ofBits modulus

The fold computes the requested modular power for every nonzero binary modulus.

theorem Complexity.BitPolynomial.frobeniusEval_pair (a modulus count : List Bool) : frobeniusEval (pair (pair a modulus) count) = frobeniusBits a modulus count

Decoding the nested pairing recovers the exact dividend, modulus, and count list.

theorem Complexity.BitPolynomial.frobeniusEval_length_le (z : List Bool) : (frobeniusEval z).length ≤ z.length

Even malformed paired inputs produce at most their input length in bits.