A common small seed test for all low-order parities

There are at most A^t nonempty subsets of at most t among A coordinates. If each such test and each of C candidates excludes at most an η fraction of seeds, their union excludes at most an A^t * C * η fraction. This is the union-bound step of Chattopadhyay and Liao, Extractors for Sum of Two Sources (2021), Lemma 5.4, before equation (5) is used on good sampler outputs. SourceReduction.Leakage supplies the individual seed bounds from the actual selected affine correlation breaker after paying the complete leakage reserve.

theorem Algebraic.Cutwidth.Extractor.card_parityTests_le_pow (ι : Type u_1) [Fintype ι] (t : ℕ) : (parityTests ι t).card ≤ Fintype.card ι ^ t

The nonempty subsets of at most t coordinates are covered by the ranges of all t-tuples. This also covers zero order and an empty type.

theorem Algebraic.Cutwidth.Extractor.card_parityBadSeeds_le {ι : Type u_1} {Choice : Type u_2} {Seed : Type u_3} [Fintype ι] [Fintype Choice] [Fintype Seed] (bad : Finset ι → Choice → Finset Seed) (t : ℕ) {η : ℝ} (hη : 0 ≤ η) (bound : ∀ U ∈ parityTests ι t, ∀ (z : Choice), ↑(bad U z).card ≤ η * ↑(Fintype.card Seed)) : ↑(parityBadSeeds bad t).card ≤ ↑(Fintype.card ι) ^ t * ↑(Fintype.card Choice) * η * ↑(Fintype.card Seed)

Union the excluded seeds over every low-order parity and every candidate position, preserving the full number of candidate choices.