Closed Cutoff Energy Claim at Constant $153$

The finite-horizon cutoff counterpart of BKL (95), with explicit envelope $b_m=153^{m-1}((m-1)!)^2$, holds at every order $m=d+1\ge2$. For every compactly supported isotropic log-concave prior, unit vector $u$, tolerance $\varepsilon>0$, and horizon $T\ge0$, there is $R_0$ such that for every $R\ge R_0$ and every ball-cutoff Eldan process satisfying CutoffEnergyClaim on a Brownian probability space,

Here $E_m$ is the cumulant energy, $p_s$ the process parameter, and $\gamma_R$ the ball cutoff. The filtration is a Brownian filtration, is constant for nonpositive times, and contains every measurable null set at time zero, exactly as required by the Lean predicate. This is the cutoff route to Theorem 4.1 formalized here; it does not assert the paper's infinite-horizon uncut identity. The literal uncut identities (68)–(73) are outside the scope of this formalization. Source: BKL arXiv:2610.05474v1, Section 6, (95).

Original Lean source

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

theorem cutoffEnergyClaim_153 : ∀ d : ℕ, 1 ≤ d → CutoffEnergyClaim 153 d :=
  cutoffEnergyClaim_of_letwinCompact LogConcave.Suspension.letwinCompactBound

Module navigation

Module: KLS/BKL/CumulantBound.

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

Supporting theorems: cumulantBoundCompact_of_cutoffEnergyClaim, cutoffEnergyClaim_all, cutoffEnergyClaim_succ, generator_cumulantEnergy_ge, letwinCompactBound.

Next: cumulantBound_153.

Source excerpt, lines 20–21 · Frozen source 408915f.