Induction over all retained-seed condense-and-split levels

The actual deterministic recursive map stays close to a conditional block source after every level. Each new seed is independent of the complete old joint law, and old approximation errors remain joint errors. The hypotheses are required only for the finitely many levels that the program runs.

theorem Algebraic.Cutwidth.Extractor.Internal.exists_recursiveBlockSource {X : Type v} {Earlier : Type u} {Fresh : ℕ → Type u} {α : ℕ → Type w} [Fintype X] [Fintype Earlier] [Nonempty Earlier] [(i : ℕ) → Fintype (Fresh i)] [∀ (i : ℕ), Nonempty (Fresh i)] [(i : ℕ) → Fintype (α i)] {t : ℕ} (initial : X → Earlier → Fin t → α 0) (C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1)) (k m e : ℕ → ℕ) (ε : ℕ → ℝ) (n : ℕ) (p : X → ℝ) (q₀ : Earlier → (Fin t → α 0) → ℝ) {η : ℝ} (sources : ∀ (y : Earlier), IsBlockSource (q₀ y) (2 ^ k 0)) (close : weightDist (weightedSeededOutput p initial) (seedFamilyWeight q₀) ≤ η) (condensers : ∀ i < n, WeightedStrongSeededCondenser (C i) (2 ^ k i) (2 ^ k i) (ε i)) (cards : ∀ i < n, Fintype.card (α (i + 1)) = 2 ^ m i) (widths : ∀ i < n, k (i + 1) ≤ m i) (entropies : ∀ i < n, m i + k (i + 1) + e i ≤ k i) : ∃ (q : RecursiveSeeds Earlier Fresh n → (Fin (recursiveBlockCount t n) → α n) → ℝ), (∀ (y : RecursiveSeeds Earlier Fresh n), IsBlockSource (q y) (2 ^ k n)) ∧ weightDist (weightedSeededOutput p (recursiveBlockMap initial C n)) (seedFamilyWeight q) ≤ η + recursiveBlockError t ε e n