Correctness and fixed widths of guarded modular squaring

The nonzero-modulus branch composes the checked multiplication and remainder semantics. Induction over the count list gives the exponent 2^count.length, while reduction after every step bounds all states independently of that exponent. The zero branch has exact width zero.

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

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

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

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

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

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

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

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