The one-shot statistical composition #
The actual selected condenser is close to a uniform mixture of conditional
flat sources of size 2^(ell+2*e). Exact serialization and a universal
binary field hash extract from each such source with error 2^(-(e+1)).
The retained-seed composition theorem adds this to the condenser's same
half-error. Both independent seeds remain visible in every final test.
theorem
Algebraic.Cutwidth.Extractor.Internal.oneShot_composition_flat
(n ell e : ℕ)
[condenserFinite : Fintype (AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)))]
[Fintype (AdjoinRoot (binaryModulus (oneShotHashExponent n ell e)))]
(P : Finset (List Bool))
(source : ∀ bits ∈ P, bits.length = n)
(threshold : 2 ^ (ell + 2 * e) ≤ P.card)
:
let m := condenserCoordinates (ell + 2 * e) (sparsePowerBits 1 (explicitCondenserBudget n (ell + 2 * e) (e + 1)));
∀
(test :
Finset
((AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) × (Fin ell → ZMod 2))),
|seededTestProb
(fun (bits : ↥P)
(seeds :
AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) =>
binaryFieldHash (oneShotHashExponent n ell e) ell
(BinaryFieldCodec.decode (oneShotHashExponent n ell e)
(encodeCondenserOutput (oneShotCondenserExponent n ell e) m
(decodedExplicitCondenser n (ell + 2 * e) (e + 1) 1 (↑bits) seeds.1)))
seeds.2)
test - uniformSeededTestProb test| ≤ (2 ^ e)⁻¹