Base Cutoff Energy Claim

Proved

FunctionalInequalities.KLS.BKL.Localization.cutoffEnergyClaim_one_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the base case $m=2$ cited in the discussion following Equation (78) and in Equation (95) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Assume the compact Letwin bound LetwinCompactBound. For every real $K\ge5$ , the cutoff-energy proposition CutoffEnergyClaim K 1 holds:

\operatorname{LetwinCompactBound}\ \Longrightarrow\ K\ge5\ \Longrightarrow\ \operatorname{CutoffEnergyClaim}(K,1).

The proposition packages the base-order energy inequality, with all of its internal quantification over compactly supported isotropic log-concave laws, unit vectors, cutoffs, and Eldan-process data. It is a base case for the subsequent induction.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem cutoffEnergyClaim_one (hL : LogConcave.Suspension.LetwinCompactBound) {K : ℝ} (hK : 5 ≤ K) :
    CutoffEnergyClaim K 1

Module navigation

Module: KLS/BKL/Localization/CutoffEnergy/Base.

Definition modules: KLS/BKL/CompactReduction, KLS/BKL/Localization/CutoffEnergy/Basic.

Selected supporting theorems: Covariance.inner_operator_self_pos_of_affineSupport_eq_top, IsEldanCutoff.ae_Q_posSemidef, IsEldanCutoff.continuous, IsEldanCutoff.dynkin, IsEldanCutoff.integrable_integral_of_ae_bound.

Previous: cumulantEnergy_one_is_one.

Source excerpt, lines 119–120 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_CutoffEnergy_Base

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.cutoffEnergyClaim_one_readable (hL : LogConcave.Suspension.LetwinCompactBound) {K : ℝ} (hK : 5 ≤ K) :
    CutoffEnergyClaim K 1 := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Theorem 4.1, p. 18; Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Equation (95), p. 25 (proof of Theorem 4.1, Section 6). Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/CutoffEnergy/Base.lean#L117-L255 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.CutoffEnergy.Base`, declaration `FunctionalInequalities.KLS.BKL.Localization.cutoffEnergyClaim_one`; the repository is private at upload time).

View graph