Correctness and polynomial time for the selected parameter schedule #
The previously checked runtime program is instantiated at the finite explicit parameters. The semantic statements retain arbitrary source and seed values; the resource proof composes unary parameter generation with the program's existing polynomial-time certificate.
theorem
Algebraic.Cutwidth.Extractor.Internal.explicitCondenserBits_length
(n k e u : ℕ)
(source seed : List Bool)
:
(explicitCondenserBits n k e u source seed).length = condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e)) * sparseFieldBits u (explicitCondenserBudget n k e)
theorem
Algebraic.Cutwidth.Extractor.Internal.explicitCondenserBits_output_rate
(n k e u : ℕ)
(source seed : List Bool)
:
u * (explicitCondenserBits n k e u source seed).length ≤ (u + 1) * k + u * sparseFieldBits u (explicitCondenserBudget n k e)
theorem
Algebraic.Cutwidth.Extractor.Internal.explicitCondenserEval_pair
(source seed n k e u : List Bool)
:
explicitCondenserEval
(Complexity.pair (Complexity.pair source seed) (Complexity.pair (Complexity.pair n k) (Complexity.pair e u))) = explicitCondenserBits n.length k.length e.length u.length source seed
theorem
Algebraic.Cutwidth.Extractor.Internal.decodedExplicitCondenser_eq
(n k e u : ℕ)
(bits : List Bool)
(seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))
:
let T := explicitCondenserBudget n k e;
let s := sparseFieldExponent u T;
have v := explicitCondenserExtensionExponent n k e u;
let r := sparsePowerBits u T;
let m := condenserCoordinates k r;
decodedExplicitCondenser n k e u bits seed = polynomialCondenser (extensionModulus s v) r m (sourcePolynomial s (explicitCondenserExtensionDegree n k e u) bits)
seed
theorem
Algebraic.Cutwidth.Extractor.Internal.decodedExplicitCondenser_addBits
(n k e u : ℕ)
(a b : List Bool)
(seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))
:
decodedExplicitCondenser n k e u (Complexity.BitPolynomial.addBits a b) seed = decodedExplicitCondenser n k e u a seed + decodedExplicitCondenser n k e u b seed
theorem
Algebraic.Cutwidth.Extractor.Internal.decodedExplicitCondenser_replicate_false
(n k e u length : ℕ)
(seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.explicitCondenserBits_mem_FP
{n k e u : List Bool → ℕ}
{source seed : List Bool → List Bool}
(hn : Complexity.UnaryFn n)
(hk : Complexity.UnaryFn k)
(he : Complexity.UnaryFn e)
(hu : Complexity.UnaryFn u)
(hsource : source ∈ Complexity.FP)
(hseed : seed ∈ Complexity.FP)
:
(fun (z : List Bool) => explicitCondenserBits (n z) (k z) (e z) (u z) (source z) (seed z)) ∈ Complexity.FP