Exact Horner semantics for a bounded block fold

A partial fold of length n ≤ total evaluates the blocks beginning at total-n, with its first block at exponent zero. This invariant makes the reverse traversal explicit and gives the full coefficient sum at n=total. The width and zero-modulus statements hold even outside this partial-fold semantic domain.

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

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

theorem Complexity.BitPolynomial.Internal.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

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

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

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

theorem Complexity.BitPolynomial.Internal.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

theorem Complexity.BitPolynomial.Internal.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

theorem Complexity.BitPolynomial.Internal.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

theorem Complexity.BitPolynomial.Internal.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

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