Condensing a block source with one shared seed

Apply a strong condenser to each of t source blocks with the same independent uniform seed. The joint output, including that seed, is within t * ε of a family of block sources at the condenser's output threshold. The source blocks may be dependent. Every ideal conditional law is a normalized block source; only the average distance over seeds is bounded. Empty seed types follow the weighted definitions' zero-mass convention.

This proves the finite block-source condensing mechanism of Chattopadhyay--Goodman--Liao, Lemma 5.5 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/download/. The proof corrects conditional tails before their heads, using correlated marginal replacement and exact averaging of conditional distances.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededCondenser.block {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] {C : α → Seed → Ω} {Kin Kout : ℕ} {ε : ℝ} (cond : WeightedStrongSeededCondenser C Kin Kout ε) {t : ℕ} {p : (Fin t → α) → ℝ} (source : IsBlockSource p Kin) : ∃ (q : Seed → (Fin t → Ω) → ℝ), (∀ (y : Seed), IsBlockSource (q y) Kout) ∧ weightDist (weightedSeededOutput p fun (x : Fin t → α) (y : Seed) (i : Fin t) => C (x i) y) (seedFamilyWeight q) ≤ ↑t * ε

A shared uniform seed condenses every block, with one copy of the seed retained and at most one condenser error per source block.