One small parity test for the fixed actual breaker

Only the genuinely used slots enter the product mask. Padding changes neither the reduction nor its parity. Every seed test is obtained from the actual selected correlation breaker and its original source reserve.

theorem Algebraic.Cutwidth.Extractor.Internal.exists_affineSourceTest (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)) (U : Finset (Fin N)) (small : U.card ≤ 4) (j : Fin N) (member : j ∈ U) (z : Fin C) : ∃ (bad : Finset (Fin (affineTestSeedBits n C a target) → Bool)), ↑bad.card ≤ (2 ^ target)⁻¹ / γ * ↑(Fintype.card (Fin (affineTestSeedBits n C a target) → Bool)) ∧ ∀ (b : Fin n → Bool), S b j z ∉ bad → |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 * γ