Successive splitting of dependent blocks

Repair the first pair while retaining its original joint cap. Correlated head replacement then preserves the input threshold of every remaining conditional block. Induction splits those tails, and the two repaired head coordinates can be prepended at the output threshold. Distance contraction and conditional averaging charge one local repair error per input block.

theorem Algebraic.Cutwidth.Extractor.Internal.blockSource_split {α : Type u_1} [Fintype α] (Kin Kout : ℕ) (δ : ℝ) (repair : ∀ (w : α × α → ℝ), IsProbabilityWeight w → CappedWeight w Kin → ∃ (v : α × α → ℝ), IsProbabilityWeight v ∧ CappedWeight v Kin ∧ IsBlockSource (fun (x : Fin 2 → α) => v (x 0, x 1)) Kout ∧ weightDist w v ≤ δ) {t : ℕ} {p : (Fin t → α × α) → ℝ} (source : IsBlockSource p Kin) : ∃ (q : (Fin (2 * t) → α) → ℝ), IsBlockSource q Kout ∧ weightDist (mapWeight (⇑(splitBlockEquiv α t)) p) q ≤ ↑t * δ