Quarter-error extraction from the selected actual recursive construction

The finite parameter bounds pay all recursive budgets. Keeping an output prefix preserves uniformity, and increasing the source threshold to 2^(2*b) preserves the same error. Eventual claims use the proved numerical size guard.

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

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

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

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

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

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

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