Strong extraction by a finite recursive block program

An initial condenser, the supplied sequence of lossless condensers and entropy budgets, and a final strong extractor give a strong extractor for the actual deterministic recursive composition. Its tests retain every initial, level, and final seed, once each. No initial ideal witness is a premise: the initial condenser supplies that witness for every source.

The error is the initial error, the explicit internal block-error sum, and one final extraction error per leaf. Giving every local error exponent e+n+2 bounds the total by 2^(-e). These are finite statistical statements for supplied components in the recursion of Chattopadhyay--Goodman--Liao, Theorem 5.6 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/. Recursion.Scheduled supplies a concrete short-seed schedule and a uniform encoded evaluator.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededCondenser.recursiveExtractor {X : Type v} {Earlier : Type u} {Fresh : ℕ → Type u} {α : ℕ → Type w} {Last : Type z} {Ω : Type r} [Fintype X] [Fintype Earlier] [Nonempty Earlier] [(i : ℕ) → Fintype (Fresh i)] [∀ (i : ℕ), Nonempty (Fresh i)] [(i : ℕ) → Fintype (α i)] [Fintype Last] [Nonempty Last] [Fintype Ω] [Nonempty Ω] {initial : X → Earlier → α 0} {Kin : ℕ} {k m e : ℕ → ℕ} {ε : ℕ → ℝ} {ε₀ εL : ℝ} {n : ℕ} (initial_cond : WeightedStrongSeededCondenser initial Kin (2 ^ k 0) ε₀) (C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1)) (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) {E : α n → Last → Ω} (final_extract : WeightedStrongSeededExtractor E (2 ^ k n) εL) : WeightedStrongSeededExtractor (recursiveBlockExtractor initial C n E) Kin (ε₀ + recursiveBlockError 1 ε e n + ↑(recursiveBlockCount 1 n) * εL)

The actual recursive map extracts strongly from the initial input threshold, with all internal and leaf errors included in its retained-seed test bound.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededCondenser.recursiveExtractor_dyadic {X : Type v} {Earlier : Type u} {Fresh : ℕ → Type u} {α : ℕ → Type w} {Last : Type z} {Ω : Type r} [Fintype X] [Fintype Earlier] [Nonempty Earlier] [(i : ℕ) → Fintype (Fresh i)] [∀ (i : ℕ), Nonempty (Fresh i)] [(i : ℕ) → Fintype (α i)] [Fintype Last] [Nonempty Last] [Fintype Ω] [Nonempty Ω] {initial : X → Earlier → α 0} {Kin : ℕ} {k m : ℕ → ℕ} {n e : ℕ} (initial_cond : WeightedStrongSeededCondenser initial Kin (2 ^ k 0) (2 ^ (e + n + 2))⁻¹) (C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1)) (condensers : ∀ i < n, WeightedStrongSeededCondenser (C i) (2 ^ k i) (2 ^ k i) (2 ^ (e + n + 2))⁻¹) (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 + n + 2) ≤ k i) {E : α n → Last → Ω} (final_extract : WeightedStrongSeededExtractor E (2 ^ k n) (2 ^ (e + n + 2))⁻¹) : WeightedStrongSeededExtractor (recursiveBlockExtractor initial C n E) Kin (2 ^ e)⁻¹

Uniform local error exponent e+n+2 pays for the initial, internal, and leaf stages.