From conditional parity bias to sumset extraction

Apply the majority bound separately at each good second-source fixing, then aggregate the ordered source pairs. This proves the final analytic step of the constant-error route. The source-reduction construction that must supply the parity-bias hypotheses is not assumed to have been built.

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