Correct evaluation of runtime coefficient blocks

For every nonzero binary modulus, the evaluator computes sum_{j<count} ofBits(block j) * ofBits(seed)^j modulo that modulus. The coefficient blocks are consecutive low-to-high slices of one flat bit string. Short or absent blocks contribute implicit high zeros. Width zero, count zero, padded inputs, and constant-one moduli are covered.

The Horner fold runs from high coefficient indices to low indices, retaining exactly the modulus degree in bits. Its partial-fold theorem explicitly requires the remaining count length to be at most the total count. A zero modulus returns the empty list. The machine certificate is in Complexitylib.Classes.P.BitPolynomial.BlockEval.

theorem Complexity.BitPolynomial.coefficientBlock_length_le (coeffs : List Bool) (width j : ℕ) : (coefficientBlock coeffs width j).length ≤ width

A coefficient slice never exceeds its requested width.

theorem Complexity.BitPolynomial.blockEvalStep_length (coefficient seed modulus state : List Bool) : (blockEvalStep coefficient seed modulus state).length = significantLength modulus - 1

Each guarded Horner step restores the modulus-degree width.

theorem Complexity.BitPolynomial.blockEvalScan_length (coeffs : List Bool) (width : ℕ) (seed modulus : List Bool) (total : ℕ) (count : List Bool) : (blockEvalScan coeffs width seed modulus total count).length = significantLength modulus - 1

Every partial fold has the same width, including the initial zero state.

theorem Complexity.BitPolynomial.blockEvalBits_length (coeffs : List Bool) (width : ℕ) (seed modulus count : List Bool) : (blockEvalBits coeffs width seed modulus count).length = significantLength modulus - 1

The full evaluator has exact modulus-degree output width.

theorem Complexity.BitPolynomial.blockEvalBits_length_le (coeffs : List Bool) (width : ℕ) (seed modulus count : List Bool) : (blockEvalBits coeffs width seed modulus count).length ≤ modulus.length

The output is at most the supplied modulus length, for all inputs.

theorem Complexity.BitPolynomial.blockEvalBits_of_modulus_zero (coeffs : List Bool) (width : ℕ) (seed modulus count : List Bool) (zero : ofBits modulus = 0) : blockEvalBits coeffs width seed modulus count = []

A zero modulus gives empty output for every coefficient string, seed, and count.

theorem Complexity.BitPolynomial.ofBits_blockEvalStep (coefficient seed modulus state : List Bool) (nonzero : ofBits modulus ≠ 0) : ofBits (blockEvalStep coefficient seed modulus state) = (ofBits coefficient + ofBits seed * ofBits state) %ₘ ofBits modulus

A Horner step adds the next coefficient to the seed times the prior state.

theorem Complexity.BitPolynomial.ofBits_blockEvalScan (coeffs : List Bool) (width : ℕ) (seed modulus : List Bool) (total : ℕ) (count : List Bool) (nonzero : ofBits modulus ≠ 0) (bound : count.length ≤ total) : ofBits (blockEvalScan coeffs width seed modulus total count) = (∑ j ∈ Finset.range count.length, ofBits (coefficientBlock coeffs width (total - count.length + j)) * ofBits seed ^ j) %ₘ ofBits modulus

A partial fold evaluates the highest requested blocks, starting at exponent zero.

theorem Complexity.BitPolynomial.ofBits_blockEvalBits (coeffs : List Bool) (width : ℕ) (seed modulus count : List Bool) (nonzero : ofBits modulus ≠ 0) : ofBits (blockEvalBits coeffs width seed modulus count) = (∑ j ∈ Finset.range count.length, ofBits (coefficientBlock coeffs width j) * ofBits seed ^ j) %ₘ ofBits modulus

The full fold equals the coefficient-block power sum modulo the runtime modulus.

theorem Complexity.BitPolynomial.blockEval_pair (coeffs widthWord seed modulus count : List Bool) : blockEval (pair (pair (pair coeffs widthWord) (pair seed modulus)) count) = blockEvalBits coeffs widthWord.length seed modulus count

The codec supplies all five runtime inputs, with width given by its word length.

theorem Complexity.BitPolynomial.blockEval_length_le (z : List Bool) : (blockEval z).length ≤ z.length

The total encoded evaluator's output is bounded by its input length.