A uniform Gamma extractor with an explicit Boolean seed budget

The actual total polynomial-time program takes 8*b source bits and exactly 2^27 * (Nat.clog 2 (b+1))^3 seed bits, and emits b bits. At every size satisfying the guard, it extracts with error at most one quarter from sources of min-entropy at least 2*b. This holds eventually in b.

The stronger weighted theorem retains the entire padded seed, including its unused suffix. The evaluator equality holds at all sizes; outside the guard the program's defined output is all false. No field instances or abstract extractor are supplied by the caller. This interface combines the CGL-based recursive construction with its proved runtime and seed-padding transport.

theorem Algebraic.Cutwidth.Extractor.gammaBlockPaddedExtractor_ofFn (b : ℕ) (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBudget b) → Bool) : List.ofFn (gammaBlockPaddedExtractor b x seed) = gammaBlockExtractorRuntime b (List.ofFn x) (List.ofFn seed)

The Boolean output vector is exactly the actual runtime's word, at every size.

theorem Algebraic.Cutwidth.Extractor.gammaBlockSeedBits_le_budget {b : ℕ} (guard : GammaBlockSizeGuard b) : gammaBlockSeedBits b ≤ gammaBlockSeedBudget b

The simple seed budget covers the actual seed tuple whenever the size guard holds.

theorem Algebraic.Cutwidth.Extractor.gammaBlockPaddedExtractor_eq (b : ℕ) (guard : GammaBlockSizeGuard b) (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBudget b) → Bool) : gammaBlockPaddedExtractor b x seed = gammaBlockExtractor b x fun (j : Fin (gammaBlockSeedBits b)) => seed (Fin.castLE ⋯ j)

At guarded sizes, the actual padded program uses precisely the required seed prefix.

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

The actual program strongly extracts while retaining every padded seed bit.

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

The same actual program is an ordinary flat seeded extractor.

theorem Algebraic.Cutwidth.Extractor.gammaBlockPaddedExtractor_eval (b : ℕ) (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBudget b) → Bool) : gammaBlockExtractorEval (Complexity.pair (List.ofFn x) (List.ofFn seed)) = List.ofFn (gammaBlockPaddedExtractor b x seed)

The existing polynomial-time paired evaluator computes every padded Boolean output.

theorem Algebraic.Cutwidth.Extractor.gammaBlockSeedBudget_unaryFn {b : List Bool → ℕ} (hb : Complexity.UnaryFn b) : Complexity.UnaryFn fun (z : List Bool) => gammaBlockSeedBudget (b z)

The complete padded seed budget can be generated in unary in polynomial time.

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

Every sufficiently large target has the full weighted retained-seed guarantee.

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

Every sufficiently large target gives an actual ordinary seeded extractor.