Selecting parity-good source fixings and coordinates

One small common seed test gives good fixings for every low-order parity at once. At each retained fixing, keep the coordinates with a candidate outside that test. This is the selection step after equation (5) in Chattopadhyay and Liao, Extractors for Sum of Two Sources (2021), Lemma 5.4.

The parity estimate is an explicit premise of this selection theorem. SourceReduction.Tests supplies it for every small parity using one fixed actual affine breaker. SourceReduction.Construction composes those tests with the actual amplified sampler and discharges the finite budgets. The conclusion retains a 1 - δ fraction of second-source fixings and discards at most a 2ε fraction of coordinates at each one. A subsequent majority application must check positivity and the moment and margin budgets.

theorem Algebraic.Cutwidth.Extractor.SomewhereSampler.exists_good_fibers {α : Type u_1} {Outer : Type u_2} {Candidate : Type u_3} {Ω : Type u_4} [Fintype α] [Fintype Outer] [Fintype Ω] {S : α → Outer → Candidate → Ω} {L ε δ : ℝ} (sampler : SomewhereSampler S L ε δ) (Q : Finset α) (positive : 0 < Q.card) (source : L ≤ ↑Q.card) (T : Finset Ω) (small : ↑T.card ≤ ε * ↑(Fintype.card Ω)) : ∃ G ⊆ Q, (1 - δ) * ↑Q.card ≤ ↑G.card ∧ ∀ y ∈ G, ↑(allHitSeeds S T y).card ≤ 2 * ε * ↑(Fintype.card Outer)

A somewhere sampler leaves many good fixings in each sufficiently large uniform source, with the same failure bound as for arbitrary source weights.

theorem Algebraic.Cutwidth.Extractor.SomewhereSampler.parity_fibers {α : Type u_1} {Source : Type u_2} {Choice : Type u_3} {Seed : Type u_4} [Fintype Source] [Fintype Choice] [Fintype Seed] {N : ℕ} {s : Finset α} {w : α → ℝ} (σ : α → Source → Fin N → ℝ) {S : Source → Fin N → Choice → Seed} {L ε δ β η : ℝ} (sampler : SomewhereSampler S L ε δ) (Q : Finset Source) (positive : 0 < Q.card) (source : L ≤ ↑Q.card) (bad : Finset (Fin N) → Choice → Finset Seed) (nonneg : 0 ≤ η) (seedBound : ∀ U ∈ parityTests (Fin N) 4, ∀ (z : Choice), ↑(bad U z).card ≤ η * ↑(Fintype.card Seed)) (budget : ↑N ^ 4 * ↑(Fintype.card Choice) * η ≤ ε) (estimate : ∀ U ∈ parityTests (Fin N) 4, ∃ j ∈ U, ∀ (z : Choice), ∀ y ∈ Q, S y j z ∉ bad U z → |weightedMean s w fun (x : α) => ∏ i ∈ U, σ x y i| ≤ β) : ∃ G ⊆ Q, (1 - δ) * ↑Q.card ≤ ↑G.card ∧ ∀ y ∈ G, ∃ (m : ℕ) (good : Fin m ↪ Fin N), ↑(N - m) ≤ 2 * ε * ↑N ∧ ParityBiasBound s w (fun (x : α) (i : Fin m) => σ x y (good i)) β

Union the bad-seed tests, apply the somewhere sampler, and retain all coordinates with an escaping candidate. The distinguished coordinate for each parity may be any member of that parity. The weights and coordinate values are arbitrary here; the majority consumer additionally needs a probability distribution, signs, and its quantitative budgets.