An actual quarter-error Gamma extractor with a polylogarithmic seed

For all sufficiently large b, the specified map takes 8*b input bits with min-entropy at least 2*b and returns b bits with error at most one quarter. The stronger weighted theorem retains the entire independent Boolean seed. Its actual length is at most 2^27 * (Nat.clog 2 (b+1))^3.

The construction instantiates the checked recursive condenser/splitting method of Chattopadhyay, Goodman, and Liao, Theorem 5.6 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/, with this library's near-halving parameters, then keeps an output prefix. These semantic guarantees use no supplied extractor or field instances. Polynomial-time evaluation is a separate layer.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractor_ofFn (b : ℕ) (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBits b) → Bool) : List.ofFn (gammaBlockExtractor b x seed) = List.take b (List.ofFn (nearHalvingBlockBooleanExtractor (8 * b) (gammaBlockDepth b) (gammaBlockReserve b) (gammaBlockErrorExponent b) x seed))

Listing the selected Gamma output takes the corresponding prefix of the actual output.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractor_weighted {b : ℕ} (guard : GammaBlockSizeGuard b) : WeightedStrongSeededExtractor (gammaBlockExtractor b) (2 ^ (2 * b)) (1 / 4)

The actual selected map strongly extracts from every capped finite weighted source.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractor_flat {b : ℕ} (guard : GammaBlockSizeGuard b) : FlatSeededExtractor (gammaBlockExtractor b) (2 ^ (2 * b)) (1 / 4)

Forgetting the retained seed gives the ordinary flat seeded-extractor contract.

theorem Algebraic.Cutwidth.Extractor.gammaBlockSeedBits_bound {b : ℕ} (guard : GammaBlockSizeGuard b) : gammaBlockSeedBits b ≤ 2 ^ 27 * gammaBlockLog b ^ 3

The selected map's actual complete seed length is bounded by a cubic logarithm.

theorem Algebraic.Cutwidth.Extractor.eventually_gammaBlockExtractor_weighted : ∀ᶠ (b : ℕ) in Filter.atTop, WeightedStrongSeededExtractor (gammaBlockExtractor b) (2 ^ (2 * b)) (1 / 4)

All sufficiently large targets have the weighted retained-seed guarantee.

theorem Algebraic.Cutwidth.Extractor.eventually_gammaBlockExtractor_flat : ∀ᶠ (b : ℕ) in Filter.atTop, FlatSeededExtractor (gammaBlockExtractor b) (2 ^ (2 * b)) (1 / 4)

All sufficiently large targets give an ordinary flat seeded extractor.

theorem Algebraic.Cutwidth.Extractor.eventually_gammaBlockSeedBits_bound : ∀ᶠ (b : ℕ) in Filter.atTop, gammaBlockSeedBits b ≤ 2 ^ 27 * gammaBlockLog b ^ 3

The actual seed lengths eventually satisfy the explicit polylogarithmic bound.