Splitting every block into successive halves

A source on t pairs, with each pair having conditional point-mass cap 2^(-k) after all earlier pairs, becomes close to a source on 2*t successive half-blocks. If each half has 2^m possible values, s ≤ m and m+s+e ≤ k give output threshold 2^s and distance at most t*2^(-e). The pairs can be dependent. Splitting uses no new random seed.

This is the finite power-of-two form of Chattopadhyay--Goodman--Liao, Corollary 5.4 of Affine Extractors for Almost Logarithmic Entropy: https://eccc.weizmann.ac.il/report/2021/075/download/. Their two-block ingredient, Lemma 5.3, credits Goldreich--Wigderson (1997). Our proof uses the explicit row repair and its preservation of the original joint cap, followed by correlated head replacement and induction on conditional tails.

This statistical theorem supplies the splitting step of the recursive extractor; the full recursive program and its parameter accounting are separate constructions.

theorem Algebraic.Cutwidth.Extractor.splitBlockEquiv_apply_fst {α : Type u_1} {t : ℕ} (x : Fin t → α × α) (i : Fin t) : (splitBlockEquiv α t) x ((splitBlockIndexEquiv t) (i, 0)) = (x i).1

The first coordinate of a pair is retained at the pair's first output position.

theorem Algebraic.Cutwidth.Extractor.splitBlockEquiv_apply_snd {α : Type u_1} {t : ℕ} (x : Fin t → α × α) (i : Fin t) : (splitBlockEquiv α t) x ((splitBlockIndexEquiv t) (i, 1)) = (x i).2

The second coordinate immediately follows the first coordinate of its pair.

theorem Algebraic.Cutwidth.Extractor.IsBlockSource.exists_split_pow_two {α : Type u_1} [Fintype α] {t m s k e : ℕ} {p : (Fin t → α × α) → ℝ} (source : IsBlockSource p (2 ^ k)) (card : Fintype.card α = 2 ^ m) (width : s ≤ m) (entropy : m + s + e ≤ k) : ∃ (q : (Fin (2 * t) → α) → ℝ), IsBlockSource q (2 ^ s) ∧ weightDist (mapWeight (⇑(splitBlockEquiv α t)) p) q ≤ ↑t * (2 ^ e)⁻¹

Split each conditional high-entropy pair into two consecutive blocks, paying at most 2^(-e) per original pair. No independence between pairs is needed.