Finite recursive block-source guarantee

The deterministic recursiveBlockMap carries an initial retained-seed approximation through any finite number of condense-and-split levels. The alphabets, seed types, entropy thresholds, and errors may vary by level. The output has 2^n*t blocks, and the previous joint error increases by the explicit sum recursiveBlockError. No bound for each individual seed is assumed. All local condenser and entropy hypotheses concern only levels strictly below n.

The seed-cardinality formula counts each level's seed once. Recursion.Scheduled supplies a concrete short-seed parameter schedule (eventually_polylogBlockExtractor) and a uniform encoded evaluator (scheduledBlockExtractorEval_mem_FP).

theorem Algebraic.Cutwidth.Extractor.recursiveBlockCount_eq (t n : ℕ) : recursiveBlockCount t n = 2 ^ n * t

The number of blocks doubles at every completed level.

theorem Algebraic.Cutwidth.Extractor.recursiveSeeds_card (Earlier : Type u) (Fresh : ℕ → Type u) [Fintype Earlier] [(i : ℕ) → Fintype (Fresh i)] (n : ℕ) : Fintype.card (RecursiveSeeds Earlier Fresh n) = Fintype.card Earlier * ∏ i ∈ Finset.range n, Fintype.card (Fresh i)

Each fresh seed is counted once, regardless of the number of blocks using it.

theorem Algebraic.Cutwidth.Extractor.recursiveSeeds_card_pow_two (Earlier : Type u) (Fresh : ℕ → Type u) [Fintype Earlier] [(i : ℕ) → Fintype (Fresh i)] (n b₀ : ℕ) (b : ℕ → ℕ) (first : Fintype.card Earlier = 2 ^ b₀) (fresh : ∀ i < n, Fintype.card (Fresh i) = 2 ^ b i) : Fintype.card (RecursiveSeeds Earlier Fresh n) = 2 ^ (b₀ + ∑ i ∈ Finset.range n, b i)

For power-of-two seed alphabets, seed widths add over the completed levels.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockError_const (t n e : ℕ) (ε : ℝ) : recursiveBlockError t (fun (x : ℕ) => ε) (fun (x : ℕ) => e) n = ↑t * (2 ^ n - 1) * (ε + (2 ^ e)⁻¹)

Constant local errors have an exact finite geometric sum.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockError_dyadic_total (h E : ℕ) : (2 ^ E)⁻¹ + recursiveBlockError 1 (fun (x : ℕ) => (2 ^ E)⁻¹) (fun (x : ℕ) => E) h + ↑(recursiveBlockCount 1 h) * (2 ^ E)⁻¹ = (3 * 2 ^ h - 1) * (2 ^ E)⁻¹

One initial error, two local errors per internal block, and one per leaf give the finite coefficient 3*2^h-1.

theorem Algebraic.Cutwidth.Extractor.recursiveBlockError_dyadic_budget (h e : ℕ) : (3 * 2 ^ h - 1) * (2 ^ (e + h + 2))⁻¹ ≤ (2 ^ e)⁻¹

Increasing each error exponent by h+2 pays for all h recursive levels.

theorem Algebraic.Cutwidth.Extractor.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

The actual recursive map has a nearby conditional block-source witness, with the initial joint error and all local errors accounted for explicitly.