Retained-seed extraction after adding unused randomness

Append a fresh independent seed and use the identity output step. The retained-seed distance bound preserves the original error, including tests that inspect the unused seed. Splitting a Boolean word into its prefix and suffix gives the fixed-width padding rule.

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

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