Completing the original seeded map to injections

For each seed, retain one original source point per reached output and extend these assignments to an injection. The resulting witness changes exactly the number of source and seed pairs lost when forming the full neighbor set. Test discrepancy is bounded by these changed pairs. The choices construct a distributional witness, not an algorithm for computing the condenser.

theorem Algebraic.Cutwidth.Extractor.Internal.embedding_agree_on_range {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f : α → β) (capacity : Fintype.card α ≤ Fintype.card β) : ∃ (g : α ↪ β), ∀ b ∈ Set.range f, ∃ (x : α), f x = b ∧ g x = b

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

theorem Algebraic.Cutwidth.Extractor.Internal.card_test_sub_le_disagreement {α : Type u_1} {β : Type u_2} [Fintype α] (f g : α → β) (T : Finset β) : |↑{x : α | f x ∈ T}.card - ↑{x : α | g x ∈ T}.card| ≤ ↑{x : α | f x ≠ g x}.card

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

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