Finite block counts, seed cardinalities, and recursive error budgets

Each level doubles the number of blocks and adds one independent seed. The exact product of seed cardinalities records their cost without charging once per block. Summing the local errors gives an explicit geometric budget.

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.recursiveBlockError_succ (t : ℕ) (ε : ℕ → ℝ) (e : ℕ → ℕ) (n : ℕ) : recursiveBlockError t ε e (n + 1) = recursiveBlockError t ε e n + ↑(recursiveBlockCount t n) * (ε n + (2 ^ e n)⁻¹)

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

theorem Algebraic.Cutwidth.Extractor.Internal.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)⁻¹

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