A simultaneous family of fixed-budget seed tests

Choose a distinguished coordinate separately for each nonempty parity test, before any candidate or source shift is supplied. The resulting bad-seed family has precisely the quantifier order needed by the global somewhere-sampler selection theorem.

theorem Algebraic.Cutwidth.Extractor.Internal.affineSourceReduction_exists_tests (n N C a target : ℕ) (p : (Fin n → Bool) → ℝ) (S : (Fin n → Bool) → Fin N → Fin C → Fin (affineTestSeedBits n C a target) → Bool) (advice : Fin N × Fin C → List Bool) {γ : ℝ} (candidates : 0 < C) (advice_positive : 0 < a) (error : 0 < γ) (probability : IsProbabilityWeight p) (cap : ∀ (x : Fin n → Bool), p x ≤ (2 ^ affineLeakageSourceEntropy n (4 * C - 1) a target)⁻¹) (length : ∀ (v : Fin N × Fin C), (advice v).length = a) (injective : Function.Injective advice) (linear : ∀ (x y : Fin n → Bool) (i : Fin N) (z : Fin C), S (xorInput x y) i z = xorInput (S x i z) (S y i z)) : ∃ (bad : Finset (Fin N) → Fin C → Finset (Fin (affineTestSeedBits n C a target) → Bool)), (∀ U ∈ parityTests (Fin N) 4, ∀ (z : Fin C), ↑(bad U z).card ≤ (2 ^ target)⁻¹ / γ * ↑(Fintype.card (Fin (affineTestSeedBits n C a target) → Bool))) ∧ ∀ U ∈ parityTests (Fin N) 4, ∃ j ∈ U, ∀ (z : Fin C) (b : Fin n → Bool), S b j z ∉ bad U z → |weightedMean Finset.univ p fun (x : Fin n → Bool) => ∏ i ∈ U, if affineSourceReduction (affineTestBit n C a target) S (fun (i : Fin N) (k : Fin C) => advice (i, k)) (xorInput x b) i = true then 1 else -1| ≤ 2 * γ