GapEstimates.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Numerical estimates for the finite sparsest-cut graph

These are the final completeness and soundness inequalities in Section 7 of Constant-factor hardness of uniform sparsest cut by OpenAI.

theorem OAI.UniformSparsestCut.completeness_ratio line 17

Source documentation

A cut of capacity at most 22 whose two sides have counting mass at least 1 / 40000 lies below the completeness threshold.

theorem completeness_ratio {N z T : ℝ} (hN : 0 < N)
    (hz : (1 : ℝ) / 40000 ≤ z) (hz' : (1 : ℝ) / 40000 ≤ 1 - z)
    (hT : T ≤ 22) : T / (N ^ 2 * (z * (1 - z))) < 10 ^ 12 / N ^ 2 := by
…

theorem OAI.UniformSparsestCut.soundness_contradiction line 35

Source documentation

Variance transfer and the tether bound contradict the comparison gap for a nontrivial monochromatic-cluster cut.

theorem soundness_contradiction {κ z ν T L D : ℝ}
    (hκ : 0 < κ) (hz₀ : 0 < z) (hz₁ : z < 1) (hν : 0 ≤ ν) (hL : 0 ≤ L)
    (hsmall : T ≤ κ * (z * (1 - z)))
    (htether : 2 * κ * L ≤ T) (htransfer : z * (1 - z) ≤ 36 * ν + L)
    (hraw : D ≤ T) (hgap : 0 < ν → 100 * κ * ν < D) : False := by
…