Statistical extraction by the actual one-shot program

The pointwise correctness theorem identifies the emitted coordinates with the proved statistical composition. Rewriting under the finite test count therefore transfers the guarantee without changing the source or either retained seed.

theorem Algebraic.Cutwidth.Extractor.Internal.decodedOneShotExtractor_flat (n ell e : ℕ) [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) (test : Finset ((AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) × (Fin ell → ZMod 2))) : |seededTestProb (fun (bits : ↥P) => decodedOneShotExtractor n ell e ↑bits) test - uniformSeededTestProb test| ≤ (2 ^ e)⁻¹