Aggregating good second-source fixings

Conditional outcome mass on a large set of second-source inputs gives unconditional outcome mass on the product of the source sets. Counting ordered pairs keeps repeated XOR values with their original multiplicity. This is the finite averaging step after the majority analysis in the Chattopadhyay–Liao sumset-extractor route.

theorem Algebraic.Cutwidth.Extractor.Internal.flatSumsetExtractor_of_many_good_fibers {n K : ℕ} {f : Cslib.BooleanFunction n} {ρ θ : ℝ} (positive : 0 < K) (hρ : 0 ≤ ρ) (good : ∀ (P Q : Finset (Fin n → Bool)), K ≤ P.card → K ≤ Q.card → ∃ G ⊆ Q, θ * ↑Q.card ≤ ↑G.card ∧ ∀ y ∈ G, ∀ (b : Bool), ρ ≤ ∑ x ∈ P, if f (xorInput x y) = b then 1 / ↑P.card else 0) : FlatSumsetExtractor f K (1 / 2 - ρ * θ)