Inductive Step for the Cutoff Energy Claim

Proved

FunctionalInequalities.KLS.BKL.Localization.cutoffEnergyClaim_succ_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the inductive step for the cutoff version of BKL Section 6, including Equation (95), p. 25.

Assume the compact Letwin bound and the formal hypothesis Lemma51Bound. Let $K\ge153$ , let $m\ge3$ , and suppose that for every $r$ with $2\le r<m$ both the cutoff claim at order $r-1$ and the compact posterior cumulant bound at order $r-1$ with constant $\operatorname{envelope}(K,r)$ hold. Then the cutoff claim holds at order $m-1$ :

\operatorname{CutoffEnergyClaim}(K,m-1).

The statement is an inductive implication, not a standalone universal cumulant theorem. It combines the previously assumed lower-order cutoff and cumulant estimates with the named compact-support and generator hypotheses.

Original Lean declaration header

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

theorem cutoffEnergyClaim_succ (hL : LogConcave.Suspension.LetwinCompactBound) (h51 : Lemma51Bound)
    {K : ℝ} (hK : 153 ≤ K) {m : ℕ} (hm : 3 ≤ m)
    (ih : ∀ r : ℕ, 2 ≤ r → r < m → CutoffEnergyClaim K (r - 1))
    (ihb : ∀ r : ℕ, 2 ≤ r → r < m → LogConcave.Suspension.CumulantBoundCompact (r - 1) (envelope K r)) :
    CutoffEnergyClaim K (m - 1)

Module navigation

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

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

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

Source excerpt, lines 181–185 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_CutoffEnergy_Step

set_option maxHeartbeats 1000000

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.cutoffEnergyClaim_succ_readable (hL : LogConcave.Suspension.LetwinCompactBound) (h51 : Lemma51Bound)
    {K : ℝ} (hK : 153 ≤ K) {m : ℕ} (hm : 3 ≤ m)
    (ih : ∀ r : ℕ, 2 ≤ r → r < m → CutoffEnergyClaim K (r - 1))
    (ihb : ∀ r : ℕ, 2 ≤ r → r < m → LogConcave.Suspension.CumulantBoundCompact (r - 1) (envelope K r)) :
    CutoffEnergyClaim K (m - 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/Step.lean#L177-L383 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.CutoffEnergy.Step`, declaration `FunctionalInequalities.KLS.BKL.Localization.cutoffEnergyClaim_succ`; the repository is private at upload time).

View graph