Exact uniform evaluation of the Gamma extractor family

Under the finite size guard, the actual total runtime computes the specified Boolean Gamma extractor on every source and every exact-width seed. The paired evaluator infers b from its 8*b input bits. Both identities allow arbitrary bits after the full seed word, which the program ignores.

The guard holds eventually, so a single total string program computes this family at all sufficiently large sizes. The program's unconditional FP certificate lives in Gamma.Program; the statistical guarantee and actual seed-length bound live in Gamma. Padding to a larger fixed seed budget is a separate transport layer.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorRuntime_append_eq (b : ℕ) (guard : GammaBlockSizeGuard b) (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBits b) → Bool) (tail : List Bool) : gammaBlockExtractorRuntime b (List.ofFn x) (List.ofFn seed ++ tail) = List.ofFn (gammaBlockExtractor b x seed)

The guarded runtime computes Gamma and ignores any suffix after the exact seed word.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorRuntime_eq (b : ℕ) (guard : GammaBlockSizeGuard b) (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBits b) → Bool) : gammaBlockExtractorRuntime b (List.ofFn x) (List.ofFn seed) = List.ofFn (gammaBlockExtractor b x seed)

At the exact Boolean seed word, the guarded runtime computes every Gamma output bit.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorEval_pair_append_eq (b : ℕ) (guard : GammaBlockSizeGuard b) (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBits b) → Bool) (tail : List Bool) : gammaBlockExtractorEval (Complexity.pair (List.ofFn x) (List.ofFn seed ++ tail)) = List.ofFn (gammaBlockExtractor b x seed)

The paired evaluator recovers the target from the source length and ignores seed padding.

theorem Algebraic.Cutwidth.Extractor.gammaBlockExtractorEval_pair_eq (b : ℕ) (guard : GammaBlockSizeGuard b) (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBits b) → Bool) : gammaBlockExtractorEval (Complexity.pair (List.ofFn x) (List.ofFn seed)) = List.ofFn (gammaBlockExtractor b x seed)

The single paired string evaluator agrees with Gamma on all guarded canonical inputs.

theorem Algebraic.Cutwidth.Extractor.eventually_gammaBlockExtractorRuntime : ∀ᶠ (b : ℕ) in Filter.atTop, ∀ (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBits b) → Bool) (tail : List Bool), gammaBlockExtractorRuntime b (List.ofFn x) (List.ofFn seed ++ tail) = List.ofFn (gammaBlockExtractor b x seed)

Eventually the actual runtime computes Gamma uniformly over all sources, seeds, and padding.

theorem Algebraic.Cutwidth.Extractor.eventually_gammaBlockExtractorEval : ∀ᶠ (b : ℕ) in Filter.atTop, ∀ (x : Fin (8 * b) → Bool) (seed : Fin (gammaBlockSeedBits b) → Bool) (tail : List Bool), gammaBlockExtractorEval (Complexity.pair (List.ofFn x) (List.ofFn seed ++ tail)) = List.ofFn (gammaBlockExtractor b x seed)

One paired evaluator eventually computes the entire Gamma family, including padded seeds.