Bounds and uniformity of the runtime condenser program #
Every coordinate has the width of one base-field coefficient, including degenerate dimensions. Polynomial-time composition handles the transposes, generated trinomials, bounded modular squaring, and block evaluation. A polynomial-time concatenation supplies all requested coordinates.
theorem
Algebraic.Cutwidth.Extractor.Internal.condenserCoordinateBits_length
(coeffs halfDegree extensionCount seed powerCount : List Bool)
:
(condenserCoordinateBits coeffs halfDegree extensionCount seed powerCount).length = 2 * halfDegree.length
theorem
Algebraic.Cutwidth.Extractor.Internal.coefficientBlock_condenserBits
(coeffs halfDegree extensionCount seed stride count : List Bool)
(i : ℕ)
(hi : i < count.length)
:
Complexity.BitPolynomial.coefficientBlock (condenserBits coeffs halfDegree extensionCount seed stride count)
(2 * halfDegree.length) i = condenserCoordinateBits coeffs halfDegree extensionCount seed (List.replicate (stride.length * i) true)
theorem
Algebraic.Cutwidth.Extractor.Internal.condenserEval_pair
(coeffs halfDegree extensionCount seed stride count : List Bool)
:
condenserEval
(Complexity.pair (Complexity.pair (Complexity.pair coeffs halfDegree) (Complexity.pair extensionCount seed))
(Complexity.pair stride count)) = condenserBits coeffs halfDegree extensionCount seed stride count
theorem
Algebraic.Cutwidth.Extractor.Internal.condenserCoordinateBits_mem_FP
{coeffs halfDegree extensionCount seed powerCount : List Bool → List Bool}
(hcoeffs : coeffs ∈ Complexity.FP)
(hhalfDegree : halfDegree ∈ Complexity.FP)
(hextensionCount : extensionCount ∈ Complexity.FP)
(hseed : seed ∈ Complexity.FP)
(hpowerCount : powerCount ∈ Complexity.FP)
:
(fun (z : List Bool) => condenserCoordinateBits (coeffs z) (halfDegree z) (extensionCount z) (seed z) (powerCount z)) ∈ Complexity.FP
theorem
Algebraic.Cutwidth.Extractor.Internal.condenserBits_mem_FP
{coeffs halfDegree extensionCount seed stride count : List Bool → List Bool}
(hcoeffs : coeffs ∈ Complexity.FP)
(hhalfDegree : halfDegree ∈ Complexity.FP)
(hextensionCount : extensionCount ∈ Complexity.FP)
(hseed : seed ∈ Complexity.FP)
(hstride : stride ∈ Complexity.FP)
(hcount : count ∈ Complexity.FP)
:
(fun (z : List Bool) => condenserBits (coeffs z) (halfDegree z) (extensionCount z) (seed z) (stride z) (count z)) ∈ Complexity.FP