The parity-bias target sufficient for a constant-error sumset extractor

For each qualifying pair of source sets P, Q, on at least half the inputs in Q, select good output coordinates whose parities of orders one through four have small absolute sign expectation. The checked moment and majority arguments then give error 35/72, strictly below one half. Balanced padding supplies the density needed by the circuit theorem.

The intended source reduction is Chattopadhyay and Liao, Extractors for Sum of Two Sources (2021), Lemma 5.4 through equation (5). SourceReduction.Leakage now derives the bad-seed bound from the actual affine correlation breaker; its linear-sampler corollary bounds the component parity at escaping seeds. SourceReduction.Construction supplies the concrete global sampler, fixed affine tests, and finite budgets and applies this implication to their actual XOR reduction. This module retains the reusable implication for arbitrary reductions; the construction's eventual parameters and uniform family are separate layers.

theorem Algebraic.Cutwidth.Extractor.majority_flatSumsetExtractor_of_parity_fibers {n N K : ℕ} (reduce : (Fin n → Bool) → Fin N → Bool) (positive : 0 < K) {δ : ℝ} (hδ : 0 ≤ δ) (fibers : ∀ (P Q : Finset (Fin n → Bool)), K ≤ P.card → K ≤ Q.card → ∃ G ⊆ Q, 1 / 2 * ↑Q.card ≤ ↑G.card ∧ ∀ y ∈ G, ∃ (m : ℕ) (good : Fin m ↪ Fin N), 0 < m ∧ 100 * ↑m ^ 2 * δ ≤ 1 ∧ ParityBiasBound P (fun (x : Fin n → Bool) => 1 / ↑P.card) (fun (x : Fin n → Bool) (i : Fin m) => if reduce (xorInput x y) (good i) = true then 1 else -1) δ ∧ ↑(N - m) ≤ √↑m / 8) : FlatSumsetExtractor (fun (z : Cslib.BitString n) => Complexity.majority (reduce z)) K (35 / 72)

Conditional low-order parity bias on enough good coordinates implies sumset extraction after majority, with error 35/72. The selected coordinates may depend on both source sets and the second-source fixing, while reduce is one fixed function of their XOR alone. The bound δ measures absolute sign-parity expectation, twice the corresponding Boolean probability bias.