The one-shot extractor on blocks with shared field seeds

Apply the actual decoded one-shot program to every block, reusing its pair of independent field seeds across all blocks. At threshold 2^(ell+2*e) per source block, the joint seed-output test error is at most t * 2^(-e) against uniform t-tuples of ell-bit outputs. The seed pair is retained once in every test.

This supplies a concrete statistical leaf for the shared-seed block argument of Chattopadhyay--Goodman--Liao, Lemma 5.5, using the checked one-shot program: https://eccc.weizmann.ac.il/report/2021/075/. OneShot.Block.Program supplies the encoded runtime loop and its exact tuple semantics.

theorem Algebraic.Cutwidth.Extractor.decodedOneShotExtractor_block (n ell e : ℕ) {α : Type u_1} [Fintype α] [Fintype (AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)))] [Fintype (AdjoinRoot (binaryModulus (oneShotHashExponent n ell e)))] (input : α ↪ List Bool) (sourceLength : ∀ (x : α), (input x).length = n) {t : ℕ} {p : (Fin t → α) → ℝ} (source : IsBlockSource p (2 ^ (ell + 2 * e))) (T : Finset ((AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) × (Fin t → Fin ell → ZMod 2))) : |weightedSeededTestProb p (fun (x : Fin t → α) (seeds : AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) (i : Fin t) => decodedOneShotExtractor n ell e (input (x i)) seeds) T - uniformSeededTestProb T| ≤ ↑t * (2 ^ e)⁻¹

The actual one-shot program extracts from all encoded source blocks with one shared seed pair and total error at most the sum of the block errors.

theorem Algebraic.Cutwidth.Extractor.decodedOneShotExtractor_block_ofFn (n ell e : ℕ) [Fintype (AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)))] [Fintype (AdjoinRoot (binaryModulus (oneShotHashExponent n ell e)))] {t : ℕ} {p : (Fin t → Fin n → Bool) → ℝ} (source : IsBlockSource p (2 ^ (ell + 2 * e))) (T : Finset ((AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) × (Fin t → Fin ell → ZMod 2))) : |weightedSeededTestProb p (fun (x : Fin t → Fin n → Bool) (seeds : AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) (i : Fin t) => decodedOneShotExtractor n ell e (List.ofFn (x i)) seeds) T - uniformSeededTestProb T| ≤ ↑t * (2 ^ e)⁻¹

Arbitrarily dependent blocks of n Boolean coordinates share one one-shot seed pair, with joint test error at most t * 2^(-e).