Padding strong-extractor seeds to a fixed upper budget

Independent unused random bits do not change the strong-extraction error. The statistical test retains every seed bit, including the unused suffix. Thus an extractor with an exact seed length bounded by a simpler computed budget can use that larger seed width without changing its guarantee.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.ignoreSeed {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} {Tail : Type u_4} [Fintype α] [Fintype Seed] [Fintype Ω] [Fintype Tail] [Nonempty Seed] [Nonempty Ω] [Nonempty Tail] {E : α → Seed → Ω} {K : ℕ} {ε : ℝ} (extract : WeightedStrongSeededExtractor E K ε) : WeightedStrongSeededExtractor (fun (a : α) (seeds : Seed × Tail) => E a seeds.1) K ε

Retaining an additional independent unused seed preserves strong extraction.

theorem Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.padSeed {α : Type u_1} {Ω : Type u_2} [Fintype α] [Fintype Ω] [Nonempty Ω] {d r K : ℕ} {ε : ℝ} {E : α → (Fin d → Bool) → Ω} (extract : WeightedStrongSeededExtractor E K ε) (size : d ≤ r) : WeightedStrongSeededExtractor (fun (a : α) (seed : Fin r → Bool) => E a fun (j : Fin d) => seed (Fin.castLE size j)) K ε

A Boolean seed can be padded to any larger width while retaining the entire padded seed.