Correctness and cost of the generated binary modulus #
The concrete coefficient generator agrees with the irreducible trinomial family. Existing modular-squaring semantics then identify every bounded runtime state with the polynomial condenser's Frobenius operation.
theorem
Algebraic.Cutwidth.Extractor.Internal.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
theorem
Algebraic.Cutwidth.Extractor.Internal.ofBits_frobeniusBits_binaryModulus
(s : ℕ)
(a count : List Bool)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.frobeniusBits_binaryModulus_length
(s : ℕ)
(a count : List Bool)
:
(Complexity.BitPolynomial.frobeniusBits a (Complexity.BitPolynomial.trinomialBits (3 ^ s)) count).length = 2 * 3 ^ s
theorem
Algebraic.Cutwidth.Extractor.Internal.encodedBinaryFrobenius_pair
(a target count : List Bool)
:
encodedBinaryFrobenius (Complexity.pair (Complexity.pair a target) count) = Complexity.BitPolynomial.frobeniusBits a (Complexity.BitPolynomial.roundedTrinomialEval target) count
theorem
Algebraic.Cutwidth.Extractor.Internal.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)
theorem
Algebraic.Cutwidth.Extractor.Internal.encodedBinaryFrobenius_length
(a target count : List Bool)
:
(encodedBinaryFrobenius (Complexity.pair (Complexity.pair a target) count)).length = 2 * 3 ^ Nat.clog 3 target.length