Lossless bounds for the explicit runtime schedule #
The integer schedule pays for the requested inverse-power-of-two error. Its proved capacity and field bounds instantiate the decoded runtime condenser's finite statistical guarantee without additional parameter inequalities at the use site.
theorem
Algebraic.Cutwidth.Extractor.Internal.explicitCondenser_loss
(n k e : ℕ)
{u : ℕ}
(rate : 0 < u)
:
↑((explicitCondenserExtensionDegree n k e u - 1) * (2 ^ sparsePowerBits u (explicitCondenserBudget n k e) - 1) * condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e))) / 2 ^ sparseFieldBits u (explicitCondenserBudget n k e) ≤ (2 ^ e)⁻¹
theorem
Algebraic.Cutwidth.Extractor.Internal.decodedExplicitCondenser_flat_lossless
(n k e u : ℕ)
[Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))]
(rate : 0 < u)
(P : Finset (List Bool))
(nonempty : P.Nonempty)
(source : ∀ bits ∈ P, bits.length = n)
(size : P.card ≤ 2 ^ k)
:
let T := explicitCondenserBudget n k e;
let s := sparseFieldExponent u T;
let m := condenserCoordinates k (sparsePowerBits u T);
∃ (g : AdjoinRoot (binaryModulus s) → ↥P ↪ Fin m → AdjoinRoot (binaryModulus s)),
∀ (test : Finset (AdjoinRoot (binaryModulus s) × (Fin m → AdjoinRoot (binaryModulus s)))),
|seededTestProb (fun (bits : ↥P) => decodedExplicitCondenser n k e u ↑bits) test - seededTestProb (fun (bits : ↥P) (y : AdjoinRoot (binaryModulus s)) => (g y) bits) test| ≤ (2 ^ e)⁻¹
theorem
Algebraic.Cutwidth.Extractor.Internal.decodedExplicitCondenser_flat_mixture
(n k e u : ℕ)
[Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))]
(rate : 0 < u)
(P : Finset (List Bool))
(source : ∀ bits ∈ P, bits.length = n)
(threshold : 2 ^ k ≤ P.card)
:
let T := explicitCondenserBudget n k e;
let s := sparseFieldExponent u T;
let m := condenserCoordinates k (sparsePowerBits u T);
∃ (g :
(S : ↥(Finset.powersetCard (2 ^ k) P)) → AdjoinRoot (binaryModulus s) → ↥↑S ↪ Fin m → AdjoinRoot (binaryModulus s)),
∀ (test : Finset (AdjoinRoot (binaryModulus s) × (Fin m → AdjoinRoot (binaryModulus s)))),
|seededTestProb (fun (bits : ↥P) => decodedExplicitCondenser n k e u ↑bits) test - seededMixtureTestProb
(fun (x : ↥(Finset.powersetCard (2 ^ k) P)) => (↑(Finset.powersetCard (2 ^ k) P).card)⁻¹)
(fun (S : ↥(Finset.powersetCard (2 ^ k) P)) (bits : ↥↑S) (y : AdjoinRoot (binaryModulus s)) => (g S y) bits)
test| ≤ (2 ^ e)⁻¹