PrincipalResponseBudgetScales

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.

Provider: the two Orlicz scales of e.new.induction.for.shom

The induction hypothesis d.mathcalS.def of ABK26 controls mathcalE_{s,infinity,2} by a sum of two one-sided weak-Orlicz terms, with scales

  A_1(s) = E s^{-1} gamma^{1/2}          (class Gamma_2) ,
  A_2(s) = s^{-2} exp(-E^{-3} gamma^{-1})  (class Gamma_{1/2}) .

The budget delta <=^2 |log gamma|^2 gamma is the statement that the first scale alone dictates the answer: A_1(s)^2 is exactly E^2 s^{-2} gamma, which at s = |log gamma|^{-1} is the printed E^2 |log gamma|^2 gamma. This module proves that in the parameter regime of the lemma the heavy scale is dominated by the light one,

  A_2(s) <= A_1(s) ,

so that no separate constant survives from the Gamma_{1/2} leg.

The regime, and where it comes from

l.approximate.recurrence.formula (label) assumes e.lower.bound.cgamma.cond.again.0: E >= C cstar^{-1} and gamma <= E^{-5}, with the constant C = C(d) still free at that point in the manuscript (it is fixed inside the proof, at e.cgamma.constraints, label). Two hypotheses are used below:

• hgamE : gamma <= (E^5)^{-1} -- literally the second half of e.lower.bound.cgamma.cond.again.0;
• h : 6 <= E -- a numerical floor on the manuscript's own free constant. It is what E >= C cstar^{-1} delivers once cstar <= 1; that last inequality is a separately tracked development gap and is not used here, the floor being taken as an explicit hypothesis instead.

The window hypothesis 8 gamma <= s is the left endpoint of the induction window s in [8 gamma, 1] of e.new.induction.for.shom itself.

Why the window enters

At s = 1 the inequality A_2 <= A_1 would read exp(-E^{-3}gamma^{-1}) <= E gamma^{1/2}, which the linear minorant of exp already gives. The honest amplitude of the heavy leg carries s^{-2}, so the worst case of the window is s = 8 gamma, where the required inequality is exp(-u) <= 8 E gamma^{3/2}. The quintic minorant u^5 <= 3125 exp u (quintic_le_exp, proved from 1 + x <= exp x at x = u/5) closes it with room to spare once E >= 6: the numerical content is 9765625 <= 64 E^7, and 64 * 6^7 = 17915904.

Scope

Everything here is elementary real analysis in three free reals E, gamma, s. Nothing refers to the model, the cube, the probe or the induction state, and no source node is claimed. Following the development convention, no numeric tactic is applied to a term containing Real.exp, Real.log or Real.rpow: the transcendental step is isolated in quintic_le_exp, and the polynomial core in the private window_leg_algebra.

Main results

• quintic_le_exp: u^5 <= 3125 exp u on [0, infinity).
• exp_leg_le_window_gaussian_leg: A_2(s) <= A_1(s) on the induction window, in the regime 6 <= E, gamma <= E^{-5}.

References

• ABK26, d.mathcalS.def, e.new.induction.for.shom.
• ABK26, the labels l.approximate.recurrence.formula, e.lower.bound.cgamma.cond.again.0, e.cgamma.constraints, d.mathcalS.def, e.new.induction.for.shom.
• ABK26 (the budget).

A quintic minorant of the exponential

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.quintic_le_exp {u : ℝ} (hu : 0 ≤ u) : u ^ 5 ≤ 3125 * Real.exp u

u^5 <= 3125 exp u for u >= 0, from 1 + x <= exp x at x = u/5. This is the only transcendental input of the module.

The polynomial core

The heavy Orlicz leg is dominated by the light one

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exp_leg_le_window_gaussian_leg {E gam s : ℝ} (hE6 : 6 ≤ E) (hgam : 0 < gam) (hgamE : gam ≤ (E ^ 5)⁻¹) (hs8 : 8 * gam ≤ s) : s⁻¹ ^ 2 * Real.exp (-(E⁻¹ ^ 3 * gam⁻¹)) ≤ E * s⁻¹ * √gam

The heavy scale of e.new.induction.for.shom is below the light one, on the induction window and in the regime of l.approximate.recurrence.formula.

  s^{-2} exp(-E^{-3} gamma^{-1})  <=  E s^{-1} gamma^{1/2} .

The hypotheses are the manuscript's own gamma <= E^{-5} of e.lower.bound.cgamma.cond.again.0, the left endpoint 8 gamma <= s of the induction window, and the numerical floor 6 <= E on the free constant of that same parameter condition.