Problem 6: Large epsilon-light vertex subsets -- Coloring Framework

PartialColoring structure, pigeonhole bound, coloring_step_exists, coloring_iterate, and barrier_parameter_bound.

Main definitions

• Problem6.PartialColoring: partial vertex coloring

Main theorems

• Problem6.largest_color_class_bound: pigeonhole bound
• Problem6.coloring_step_exists: one-step coloring extension
• Problem6.coloring_iterate: k-step coloring iteration
• Problem6.barrier_parameter_bound: final parameter bound

Coloring process

structure Problem6.PartialColoring (V : Type u_2) [Fintype V] (r : ℕ) : Type u_2

A coloring of a subset T ⊆ V with r colors.

• colored : Finset V

  The set of colored vertices

• color : V → Fin r

  The color assignment function

theorem Problem6.largest_color_class_bound {V : Type u_1} [Fintype V] {r : ℕ} (pc : PartialColoring V r) (hr : 0 < r) : ∃ (γ : Fin r), {v ∈ pc.colored | pc.color v = γ}.card * r ≥ pc.colored.card

The largest color class in a coloring has size at least |T|/r (pigeonhole).

The inductive coloring step

theorem Problem6.coloring_step_exists {V : Type u_1} [Fintype V] [DecidableEq V] (ε : ℝ) (hε : 0 < ε) (_hε1 : ε ≤ 1) (n : ℕ) (hn : 4 ≤ n) (r : ℕ) (hr_def : r = ⌈16 / ε⌉₊) (A : V → Fin r → Matrix V V ℝ) (_hA_psd : ∀ (v : V) (γ : Fin r), (A v γ).PosSemidef) (t : ℕ) (_ht : t < n / 4) (pc : PartialColoring V r) (hcard : pc.colored.card = t) (hcard_le : t < Fintype.card V) (u_t : ℝ) (hu_t : u_t = ε / 2 + ↑t * (ε / ↑n)) (hA_small : ∀ (v : V), ∃ (γ : Fin r), ((ε / ↑n) • 1 - A v γ).PosSemidef) (hbarrier : ∀ (γ : Fin r), (u_t • 1 - ∑ v ∈ pc.colored with pc.color v = γ, A v γ).PosSemidef) : have u_t' := ε / 2 + (↑t + 1) * (ε / ↑n); ∃ (pc' : PartialColoring V r), pc'.colored.card = t + 1 ∧ pc.colored ⊆ pc'.colored ∧ ∀ (γ : Fin r), (u_t' • 1 - ∑ v ∈ pc'.colored with pc'.color v = γ, A v γ).PosSemidef

Coloring step: Given a partial coloring of t vertices satisfying the per-color PSD barrier invariant at level u_t, and given t < k < n, there exists a way to extend the coloring by one vertex such that the invariant holds at level u_{t+1}. The proof uses averaging: the average barrier cost over all (vertex, color) choices is < 1 (by averaging_step), so some valid (v, γ) choice exists. Then one_sided_barrier ensures the barrier condition propagates. This is the core mathematical step of the coloring construction.

theorem Problem6.coloring_iterate {V : Type u_1} [Fintype V] [DecidableEq V] (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (hn : 4 ≤ n) (hn_eq : n = Fintype.card V) (r : ℕ) (hr_def : r = ⌈16 / ε⌉₊) (A : V → Fin r → Matrix V V ℝ) (hA_psd : ∀ (v : V) (γ : Fin r), (A v γ).PosSemidef) (hA_small : ∀ (v : V), ∃ (γ : Fin r), ((ε / ↑n) • 1 - A v γ).PosSemidef) (k : ℕ) (hk : k = n / 4) : have u_k := ε / 2 + ↑k * (ε / ↑n); ∃ (pc : PartialColoring V r), pc.colored.card = k ∧ ∀ (γ : Fin r), (u_k • 1 - ∑ v ∈ pc.colored with pc.color v = γ, A v γ).PosSemidef

Coloring iteration: Apply coloring_step_exists k times to build a partial coloring of k = n/4 vertices satisfying the barrier invariant. Starting from the empty coloring (t = 0, u_0 = ε/2), we iteratively extend the coloring. At each step, coloring_step_exists provides the next coloring. After k steps, we have a coloring of k vertices with the barrier invariant at u_k.

theorem Problem6.barrier_parameter_bound (ε : ℝ) (hε : 0 < ε) (n : ℕ) (hn : 4 ≤ n) : have k := n / 4; have u₀ := ε / 2; have δ := ε / ↑n; have u_k := u₀ + ↑k * δ; u_k ≤ 3 * ε / 4 ∧ 3 * ε / 4 < ε

Parameter bound (Step 3): The final barrier parameter u_k = eps/2 + k*(eps/n) satisfies u_k <= 3eps/4 < eps when k = n/4 and n >= 4. Proof: u_k = eps/2 + (n/4)(eps/n). Since n/4 <= n/4 (integer division), (n/4)(eps/n) <= (n/4)(eps/n) = eps/4. So u_k <= eps/2 + eps/4 = 3*eps/4 < eps.