Problem 6: Large epsilon-light vertex subsets -- Main Proof #
This file contains the main theorem and its supporting lemmas.
All auxiliary infrastructure is in Problem6Aux.lean.
Main theorems #
Problem6.exists_eps_light_subset: for every simple graph G andepsilon in (0,1], there exists an epsilon-light subset S with|S| >= epsilon/256 * |V|
BSS coloring infrastructure #
The BSS framework follows the informal proof's dynamic approach:
- Spectral setup: Lhalf with Lhalf² = L (via spectral theorem)
- Normalized edge Laplacians A_e = Lhalf_pinv * L_e * Lhalf_pinv
- Coloring with one-sided barrier tracking monochromatic matrix M_t
- Pullback: M_k ≤ u_k·I → each color class ε-light (via eps_light_of_loewner_bound)
Product of unitary-diagonal-conjugate matrices: (U * D(f) * U★) * (U * D(g) * U★) = U * D(f·g) * U★. Used for spectral calculus (computing products via eigenvalue multiplication).
Sub-lemma 1 (Spectral setup): For any graph G, there exists a Hermitian matrix Lhalf with Lhalf * Lhalf = graphLaplacian G (the PSD square root), constructed via the spectral theorem. This is Step 1 of the informal proof. The spectral decomposition L = U * diag(λ) * U* gives Lhalf = U * diag(√λ) * U*, which satisfies Lhalf² = L and IsHermitian.
For a Hermitian matrix M, there exists a Hermitian pseudo-inverse M_pinv satisfying the Moore-Penrose conditions: (1) M * M_pinv * M = M (2) M_pinv * M * M_pinv = M_pinv (3) M * M_pinv is idempotent (a projection) Constructed via spectral decomposition: if M = U * diag(λ) * U★, then M_pinv = U * diag(λ⁻¹) * U★ where λ⁻¹(i) = 0 if λ(i) = 0.
Dynamic BSS coloring (Steps 1–5 combined) #
The informal proof (Steps 3–5) uses a dynamic coloring process:
- Per-edge matrices: A_e := L^{-1/2} L_e L^{-1/2} with ∑_e A_e = I on range(L)
- Track M_t := ∑_{monochromatic edges at time t} A_e (DYNAMIC, depends on current coloring)
- At time t: color vertex v with γ, increment M_{t+1} = M_t + B_v^γ where B_v^γ = ∑{u ∈ T, col(u)=γ, uv∈E} A{uv}
- BSS barrier (Lemma 6.1) maintains M_t ≺ u_t·I at each step
- After k = n/4 steps: M_k = ∑a L^{-1/2} L{S_a} L^{-1/2} (by construction)
- Since M_k ≺ u_k·I ≺ ε·I, each color class S_a is ε-light
The proof is decomposed into:
(A)
dynamic_barrier_coloring: The core BSS dynamic coloring induction that produces a PartialColoring with per-color barrier bounds on normalized monochromatic sums. (B)bss_dynamic_coloring: Combines (A) withpinv_pullback_eqandeps_light_of_loewner_boundto convert barrier bounds to ε-lightness.
Off-diagonal entry equality for the cross-edge decomposition: for i ≠ j, (graphLaplacian G - DS) i j = (graphLaplacian G_same) i j.
Diagonal entry derivation for the cross-edge decomposition: derives diagonal from row sums and off-diagonal matching.
The cross-edge sum decomposition is PSD: the difference between the graph Laplacian and the double sum ∑{v uncolored} ∑γ (L{S_γ ∪ {v}} - L{S_γ}) is PSD, equaling the Laplacian of the "same-status" subgraph (edges where both endpoints have the same colored/uncolored status).
Base case of BSS induction: empty coloring, M_0 = 0, Φ_{ε/2}(0) = 2n/ε.
BSS averaging: ∃ good (v₀, γ₀) pair with barrier conditions. Core by_contra argument of the BSS dynamic coloring.
BSS induction step: extend coloring by one vertex using good_pair_exists.
Total barrier bound (Steps 3-4 of informal proof, core BSS): Given the spectral
setup, there exists a partial coloring of k = n/4 vertices with r = ⌈16/ε⌉ colors
such that the TOTAL monochromatic normalized sum ∑_γ M_γ ≤ u_k · I.
The per-color bounds then follow from psd_sub_sum_le (extraction lemma).
The proof constructs the coloring step by step using one_sided_barrier:
- Track M_t = ∑_γ M_t^γ (total monochromatic matrix, eq. 38)
- At step t, for each (v,γ) ∈ R × [r], the increment B_v^γ increases M_t^γ
- Averaging: ∑_{v,γ} B_v^γ ≤ P ≤ I (sum of cross-edge contributions)
- By
trace_mul_le_of_loewner+barrier_potential_decrease+ averaging: average barrier cost < 1, so some (v,γ) satisfies the barrier condition (eq. 35) - Apply
one_sided_barrierto propagate M_t ≺ u_t·I → M_{t+1} ≺ u_{t+1}·I - After k steps: (u_k·I - M_k).PosDef implies (u_k·I - ∑_γ M_k^γ).PosSemidef
Dynamic barrier coloring (Steps 3-4 of informal proof): Given the spectral setup
(Lhalf, Lhalf_pinv satisfying Moore-Penrose conditions), there exists a partial coloring
of k = n/4 vertices with r = ⌈16/ε⌉ colors such that each color class γ has its
normalized monochromatic matrix bounded: Lhalf_pinv * L_{S_γ} * Lhalf_pinv ≼ u_k · I.
Proof: Apply total_barrier_bound for the total sum bound ∑_γ M_γ ≤ u_k·I,
then psd_sub_sum_le to extract per-color bounds (since each M_γ is PSD).
Dynamic BSS coloring result (Steps 1–5 of informal proof): Given the spectral
setup (Lhalf with Lhalf² = L), there exists a partial coloring of k = n/4 vertices
with r = ⌈16/ε⌉ colors such that each color class is ε-light.
Proof: Obtain Lhalf_pinv from hermitian_pseudo_inverse_exists, apply
dynamic_barrier_coloring for the barrier bound, then use pinv_pullback_eq
and eps_light_of_loewner_bound to convert the barrier bound to ε-lightness.
The BSS coloring result (correctly stated, dynamic approach). There exists a partial coloring of n/4 vertices with r = ⌈16/ε⌉ colors such that each color class is ε-light. This captures Steps 1–5 of the informal proof:
spectral_sqrt_exists: Construct Lhalf with Lhalf² = L (spectral setup)bss_dynamic_coloring: Dynamic coloring with per-edge tracking
The coloring induction result #
The result of the BSS coloring induction: there exists a partial coloring of k vertices
with r colors such that each color class is ε-light. This packages Steps 1-5 of the
informal proof, delegating to bss_coloring_eps_light which uses:
spectral_sqrt_exists: Lhalf with Lhalf² = Lbss_dynamic_coloring: Dynamic per-edge coloring with BSS barrier
Proof of the main theorem #
For n ≥ 4, the coloring process produces an ε-light set of size ≥ εn/256.
For 1 ≤ n ≤ 3, a single vertex is ε-light and satisfies the size bound.
Main theorem #
Main Theorem (Problem 6): For every simple graph G on a finite vertex set V and every ε ∈ (0, 1], there exists an ε-light subset S with |S| ≥ ε/256 · |V|.