Exact program output and uniform seed padding

The runtime has exactly the requested output length. Its unused seed suffix does not affect the canonical output, so retaining independent padding preserves the strong guarantee. All runtime identities cover every word size.

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

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

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

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

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

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

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

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

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