A finite recursive block extractor #
An initial condenser produces one block. Each recursive level applies its condenser with one shared fresh seed and splits the resulting pairs. A final extractor uses one further seed on every leaf block. All these seeds remain in the seed type, and the output is the complete tuple of leaf outputs.
This is the deterministic finite composition underlying Chattopadhyay--Goodman--Liao, Theorem 5.6 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/. The component maps are supplied; an encoded evaluator and numerical short-seed schedule are separate constructions.
def
Algebraic.Cutwidth.Extractor.recursiveBlockExtractor
{X : Type v}
{Earlier : Type u}
{Fresh : ℕ → Type u}
{α : ℕ → Type w}
{Last : Type z}
{Ω : Type r}
(initial : X → Earlier → α 0)
(C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1))
(n : ℕ)
(E : α n → Last → Ω)
:
X → RecursiveSeeds Earlier Fresh n × Last → Fin (recursiveBlockCount 1 n) → Ω
Initial condensation, recursive shared-seed splitting, and shared-seed leaf extraction.
Equations
- One or more equations did not get rendered due to their size.