Uniform encoded construction of the binary modulus family

The runtime trinomial generator constructs the monic irreducible family X^(2 * 3^s) + X^(3^s) + 1. Rounding a requested unary half-degree costs at most a factor of three, with a constant allowance at the empty input. The single evaluator generates that modulus and performs modular squaring in polynomial time in the dividend, target, and unary squaring-count lengths.

This connects the concrete bit-list arithmetic to modularFrobenius. Condenser.Encoding.Correctness uses the extension-field packing to assemble the complete seeded condenser evaluator. No search through a field or irreducible polynomials is used.

theorem Algebraic.Cutwidth.Extractor.ofBits_trinomialBits_pow_three (s : ℕ) : Complexity.BitPolynomial.ofBits (Complexity.BitPolynomial.trinomialBits (3 ^ s)) = binaryModulus s

The sparse coefficient generator is the explicit irreducible binary family.

theorem Algebraic.Cutwidth.Extractor.ofBits_roundedTrinomialEval (target : List Bool) : Complexity.BitPolynomial.ofBits (Complexity.BitPolynomial.roundedTrinomialEval target) = binaryModulus (Nat.clog 3 target.length)

Rounding the requested half-degree chooses the corresponding family member.

theorem Algebraic.Cutwidth.Extractor.roundedTrinomialEval_degree_bounds (target : List Bool) : 2 * target.length ≤ (Complexity.BitPolynomial.ofBits (Complexity.BitPolynomial.roundedTrinomialEval target)).natDegree ∧ (Complexity.BitPolynomial.ofBits (Complexity.BitPolynomial.roundedTrinomialEval target)).natDegree ≤ 6 * target.length + 2

The generated degree covers the target with a linear bound, even at zero.

theorem Algebraic.Cutwidth.Extractor.ofBits_frobeniusBits_binaryModulus (s : ℕ) (a count : List Bool) : Complexity.BitPolynomial.ofBits (Complexity.BitPolynomial.frobeniusBits a (Complexity.BitPolynomial.trinomialBits (3 ^ s)) count) = modularFrobenius (binaryModulus s) count.length (Complexity.BitPolynomial.ofBits a)

Encoded modular squaring agrees with the condenser's polynomial operation.

theorem Algebraic.Cutwidth.Extractor.frobeniusBits_binaryModulus_length (s : ℕ) (a count : List Bool) : (Complexity.BitPolynomial.frobeniusBits a (Complexity.BitPolynomial.trinomialBits (3 ^ s)) count).length = 2 * 3 ^ s

Every encoded state occupies exactly one binary field element.

theorem Algebraic.Cutwidth.Extractor.encodedBinaryFrobenius_pair (a target count : List Bool) : encodedBinaryFrobenius (Complexity.pair (Complexity.pair a target) count) = Complexity.BitPolynomial.frobeniusBits a (Complexity.BitPolynomial.roundedTrinomialEval target) count

The public evaluator reads the dividend, half-degree target, and count.

theorem Algebraic.Cutwidth.Extractor.ofBits_encodedBinaryFrobenius (a target count : List Bool) : Complexity.BitPolynomial.ofBits (encodedBinaryFrobenius (Complexity.pair (Complexity.pair a target) count)) = modularFrobenius (binaryModulus (Nat.clog 3 target.length)) count.length (Complexity.BitPolynomial.ofBits a)

Generating the modulus and then running the loop computes modular Frobenius.

theorem Algebraic.Cutwidth.Extractor.encodedBinaryFrobenius_length (a target count : List Bool) : (encodedBinaryFrobenius (Complexity.pair (Complexity.pair a target) count)).length = 2 * 3 ^ Nat.clog 3 target.length

The evaluator's output has the generated field's exact bit width.

theorem Algebraic.Cutwidth.Extractor.encodedBinaryFrobenius_mem_FP : encodedBinaryFrobenius ∈ Complexity.FP

Modulus construction and modular squaring form one uniform polynomial-time program.