KLS endpoint: Poincaré constant 500 and Cheeger coefficient 1.97

The final endpoint is independently accepted. The user-requested stopping threshold has been reached: the Cheeger conversion coefficient is 1.97 < 2, with our dimension-free Poincaré constant 500.

The achieved target is the dimension-free pair

$$ \operatorname{Var}_\mu(f)\le500\int\|\nabla f\|^2\,d\mu, \qquad h(\mu)\ge\frac{100}{197\sqrt{500}} =\frac1{1.97\sqrt{500}}. $$

The displayed finite-energy Poincaré theorem covers locally Lipschitz functions with finite energy; the exact OpenAI statement uses smooth compactly supported tests. Here 1.97 is the conversion coefficient, and $h(\mu)$ is the original closed-neighborhood Cheeger constant. The coefficient is strictly below 2. The final Cheeger theorem applies to every original admissible isotropic log-concave law in every positive dimension, including nonsmooth densities and bounded or unbounded supports. Its conclusion has no extra smoothness, curvature, finite-iteration or scalar-profile hypothesis. Both original full Cheeger law formulations are covered. No optimal-constant claim is needed or made. This is the user-requested stopping point.

Exact Lean endpoints

OpenAI's Model at commit adc7f1241b42e322a6451854ab7e4b4c146bf78a is preserved byte for byte, with SHA-256 28cddbf3c493afd43b3f7aba78f670952ea0c38909665c86bff883849e7f8dbc. Its genuine dimension-free statement places one positive constant before every dimension and density quantifier:

def KLSStatement : Prop :=
  ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 1 ≤ n →
    ∀ ρ : Space n → ℝ, IsLogConcaveDensity ρ → IsIsotropic (densityMeasure ρ) →
      PoincareBound (densityMeasure ρ) C

The fixed witness is our proved constant 500. These are the independently accepted original endpoint types:

OAI.LeanBlast.KLS.poincareBound500 (n : ℕ) :
  1 ≤ n →
    ∀ (ρ : OAI.LeanBlast.KLS.Space n → ℝ),
      OAI.LeanBlast.KLS.IsLogConcaveDensity ρ →
        OAI.LeanBlast.KLS.IsIsotropic (OAI.LeanBlast.KLS.densityMeasure ρ) →
          OAI.LeanBlast.KLS.PoincareBound (OAI.LeanBlast.KLS.densityMeasure ρ) 500

OAI.LeanBlast.KLS.klsStatement500 : OAI.LeanBlast.KLS.KLSStatement

OAI.LeanBlast.KLS.fullStatement500 : OAI.LeanBlast.KLS.FullStatement

The full original finite-energy endpoint also derives square-integrability and integrability of the squared gradient before asserting the real-integral inequality:

KLS.admissibleMeasure.real_poincare_coupledRankYoung {n : ℕ} (hn : 1 ≤ n) {μ : MeasureTheory.Measure (KLS.Space n)}
  (hμ : KLS.admissibleMeasure μ) {f : KLS.Space n → ℝ} (hf : LocallyLipschitz f) (he : KLS.energy μ f < ⊤) :
  MeasureTheory.MemLp f 2 μ ∧
    MeasureTheory.Integrable (fun x => ‖gradient f x‖ ^ 2) μ ∧
      ∫ (x : KLS.Space n), f x ^ 2 ∂μ - (∫ (x : KLS.Space n), f x ∂μ) ^ 2 ≤
        500 * ∫ (x : KLS.Space n), ‖gradient f x‖ ^ 2 ∂μ

These new Cheeger and stopping-threshold types were printed by the independent final audit:

KLS.entropyCheegerCoefficient_lt_two : 197 / 100 < 2

KLS.admissibleMeasure.cheeger_lower_entropy197_500 {n : ℕ} (hn : 1 ≤ n) {μ : MeasureTheory.Measure (KLS.Space n)}
  (hμ : KLS.admissibleMeasure μ) : ENNReal.ofReal (100 / (197 * √500)) ≤ KLS.cheegerConstant μ

KLS.fullCheegerVerification_entropy197_500 : KLS.FullCheegerVerification

KLS.exactOpenAIKLSStatement_entropy197_500 : OAI.LeanBlast.KLS.KLSStatement

KLS.klsConjecture_entropy197_500 : KLS.KLSConjecture

The final source also proves the single conjunction KLS.dimensionFree500_and_cheeger197, combining the explicit OpenAI Poincaré bound 500 for every density with the Cheeger bound for every original admissible measure. The six literal endpoint types, independent receipt, and semantic review retain the complete statement and verification details.

How the coefficient falls below 2

The new argument uses actual finite powers of the weighted mass resolvent. It constructs every smooth representative and every auxiliary entropy resolvent, rather than assuming a smoothing estimate. The globally smooth degree 20 polynomial

$$ \Psi(s)=\frac{87}{100}\sum_{i=0}^{10}(-1)^i\binom{3/4}{i} \left(\frac9{10}\right)^i s^{2i} $$

obeys $3/20\le\Psi\le87/100$, $|\Psi'|\le3$, and $\Psi(-\Psi'')\ge1$ on $|s|\le1$. An exact positive Bernstein-polynomial identity proves the curvature inequality in Lean; an independent exact-rational calculation also checks every coefficient and both derivatives. The scaled profile is $B\Psi(s/B)$ on $|s|\le B$.

The Kato gradient comparison, resolvent positivity and weighted Cauchy inequality give a mixed entropy recurrence with the exact clock equation $a_{k+1}^2-a_ka_{k+1}=1$. The actual iterate lag permits a relative-profile loss of at most 1.01. After the fixed prefix, clock growth is at least 1.98 per squared step. A proved finite integer selection, total time $5C/4$ and a 51-step prefix give displacement coefficient $279/200$ and spectral contraction at most $29/100$. Thus the variance gap is at least $71/100$, and

$$ \frac{279/200}{71/100}=\frac{279}{142}<\frac{197}{100}<2. $$

Compact tests supply all initial gradient and diffusion bounds; the zero-bound case is proved separately. The existing full-law approximation and centered-shell conversion then give the displayed Cheeger theorem with the original boundary definition. The exported generic full-law theorem explicitly assumes a uniform Poincaré constant for admissible smooth strongly convex approximants. Our proved full-class membership of 500 discharges that premise. This report makes no claim about replacing 500 by each nonsmooth law's individual optimal Poincaré constant.

Correspondence with the papers and proof departures

The dimension-free isotropic Poincaré conclusion agrees with Bizeul–Klartag–Lehec v1, Theorem 1.1 and Song–Zhang v2, Theorem 9.1. The constant 500 is our certified sufficient witness; it is not presented as a numerical constant quoted from either paper.

The proof is not a line-by-line formalization of both papers. The Poincaré proof follows the BKL cumulant, suspension and Taylor-criterion route, with the quadratic-variance-eight input corresponding to Letwin v1, Theorem 1.2, and additional proved quantitative estimates. Song–Zhang's separate repeated height-reduction proof is not independently reproduced. The nonisotropic covariance-scaled BKL conclusion is outside this endpoint.

The analytic realization uses weak $C^{1,1}$ moment maps, local weak-Hessian integrability, weak integration by parts and Itô identities, cutoff approximation and weighted Hilbert-space spectral theory where the paper arguments use classical smoothness or global growth conditions. Full-law approximation removes the regularity restrictions from the final theorem. The new 1.97 Cheeger conversion is an additional finite-resolvent entropy argument with an explicit polynomial certificate; it does not import an unformalized heat-semigroup estimate. OpenAI's curvature-dependent regular Poincaré theorem is unused in the endpoint bridge. The Poincaré proof and detailed paper correspondence record the underlying constant 500 checkpoint; the present report supersedes its older Cheeger conversion.

Verification

The accepted baseline remains unchanged. Lean 4.35.0-rc3 and the pinned mathlib checkout are used at kernel trust level 0. Root freshly rebuilt all five final generic-conversion modules and their audits, then separately rebuilt the final numerical endpoint and audited the combined accepted-origin union. The combined added-module audit checks 11,298 declarations, including 10,812 theorems, across 457 declaring modules and 4,516 strict declaration-origin gates. The original 1744-module baseline and all accepted dependency source, object, log and package pins were rechecked. Full source and actual theorem-type reviews cover the numerical specialization, with two independent source reviews for the generic conversion. Every endpoint's recursively collected axiom set is exactly propext, Classical.choice, and Quot.sound; no additional mathematical axiom or admitted proof is used.