Strong flat lossless condensation from full-neighbor expansion

For a uniform source on P, retain one original source point for every reached output at each seed. If the output alphabet has at least P.card elements, these assignments extend to injections on P, separately for each seed. Thus the ideal output is uniform on P.card values conditional on every seed, and the seed itself is preserved exactly. Full-neighbor expansion bounds the fraction of changed source and seed pairs and hence the discrepancy of every seeded output test.

This is the finite support argument underlying Guruswami, Umans, and Vadhan (2009), Lemma 4.1, with completion inside each seed fiber: https://salil.seas.harvard.edu/sites/g/files/omnuum4266/files/salil/files/acm2009.pdf. The witness may depend on the source support and is not an evaluator. Extending the result to nonuniform sources requires a separate decomposition into flat sources; no such decomposition is assumed or supplied here.

theorem Algebraic.Cutwidth.Extractor.exists_seedwise_injection {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] [Fintype Ω] (C : α → Seed → Ω) (P : Finset α) (capacity : P.card ≤ Fintype.card Ω) : ∃ (g : Seed → ↥P ↪ Ω), {xy : ↥P × Seed | C (↑xy.1) xy.2 = (g xy.2) xy.1}.card = (seededNeighborSet C P).card

Complete one representative per reached output to an injection at each seed. The number of unchanged original pairs is exactly the neighbor count. The statement also holds for empty source, seed, and output types.

theorem Algebraic.Cutwidth.Extractor.seededTestProb_sub_le_disagreement {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (C G : α → Seed → Ω) (T : Finset (Seed × Ω)) : |seededTestProb C T - seededTestProb G T| ≤ ↑{xy : α × Seed | C xy.1 xy.2 ≠ G xy.1 xy.2}.card / (↑(Fintype.card α) * ↑(Fintype.card Seed))

Coupling two seeded maps on the same uniform source and seed bounds every test discrepancy by the fraction of pairs on which their outputs differ.

theorem Algebraic.Cutwidth.Extractor.exists_seedwise_injection_of_expansion {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] [Nonempty Seed] [Fintype Ω] (C : α → Seed → Ω) (P : Finset α) (nonempty : P.Nonempty) (capacity : P.card ≤ Fintype.card Ω) {ε : ℝ} (expansion : (1 - ε) * ↑P.card * ↑(Fintype.card Seed) ≤ ↑(seededNeighborSet C P).card) : ∃ (g : Seed → ↥P ↪ Ω), ∀ (T : Finset (Seed × Ω)), |seededTestProb (fun (x : ↥P) => C ↑x) T - seededTestProb (fun (x : ↥P) (y : Seed) => (g y) x) T| ≤ ε

Full-neighbor expansion gives error at most ε against an ideal seeded output that, conditional on each seed, is uniform on P.card distinct values.