ShellNormalization

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.

The deterministic normalization arithmetic of e.nablaw.in.L.eight

ABK26's display e.nablaw.in.L.eight is a three-line chain. After the Calderon-Zygmund step and the fresh-shell L^8 estimate e.km.kn.Lp, the manuscript's last inequality reads

  C shom_{m-h}^{-2} h 3^{2 gamma m}
    + O_{Gamma_1}( C shom_{m-h}^{-2} 3^{2 gamma m} h 3^{-(K-m) d / 8} )
  <=  C + O_{Gamma_1}( gamma^100 ) .

This module proves the two purely deterministic facts that this last line consists of, in the exact shape in which the recurrence uses them.

• inv_sigmaBarSq_mul_shellWidth_le is the deterministic head: under the induction state d.mathcalS.def and the recurrence's own shell-width constraint h <= 6 cstar gamma^{-1}, the normalized quantity shom_{m-h}^{-2} h 3^{2 gamma m} is bounded by an absolute constant `24

  • 3^18. Only the lower half of e.shom.h.boundsand the absolute bound `cstar <= 3/2` are used.

• rpow_gap_le_gammaPow_mul_spare is the fluctuation amplitude: for d >= 2, gamma <= 1/4 and a scale gap G >= 10^10 gamma^{-1} (the manuscript's e.recurrence.params), the Calderon-Zygmund decay factor 3^{-(d/8) G} is below gamma^100 with an exponentially large factor to spare. The spare factor is what absorbs the dimension-only constant, i.e. it is the quantitative content of "increasing M in e.cgamma.constraints, if necessary".

Putting the two together bounds the whole O_{Gamma_1} amplitude of the middle line by gamma^100, with no smallness assumption on gamma beyond the standing gamma <= 1/4: it is the case C = 24 * 3^18 of const_mul_rpow_gap_le_gammaPow below, whose smallness hypothesis holds there because 24 * 3^18 <= 3^21 is already swallowed by the spare factor. The composition itself is the consumer's, and is not performed here.

• const_mul_rpow_gap_le_gammaPow carries an arbitrary nonnegative prefactor C (the dimension-only constant produced by Calderon-Zygmund and by e.km.kn.Lp) under the explicit smallness hypothesis C <= 3^(10^9 / gamma), and exists_gamma_threshold_for_gap_constant shows that every C satisfies that hypothesis once gamma is small. Together they are the machine-checked form of the manuscript's parenthetical "increasing M in e.cgamma.constraints, if necessary".

Public binder audit

M : ABKModel d is standing data and d is implicit typing data. hS: inductionState M m0 E is the source induction hypothesis (d.mathcalS.def), hm : m - h <= m0 is its scale range, hh is the recurrence's own shell-width constraint, and hK is e.recurrence.params. No proof step is a binder: no Calderon-Zygmund estimate, no corrector bound, and no oscillation estimate appears as a hypothesis.

References

• ABK26, e.nablaw.in.L.eight.
• ABK26, d.mathcalS.def / e.shom.h.bounds.
• ABK26, l.approximate.recurrence.formula (the constraints h <= 6 cstar gamma^{-1} and K >= m + 10^10 gamma^{-1}).

An elementary logarithmic bound

The deterministic head

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.inv_sigmaBarSq_mul_shellWidth_le {d : ℕ} (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {m : ℤ} {h : ℕ} (hm : m - ↑h ≤ m0) (hh : ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹) : (↑(Annealed.sigmaBar M (m - ↑h)) ^ 2)⁻¹ * ↑h * 3 ^ (2 * M.gamma * ↑m) ≤ 24 * 3 ^ 18

The deterministic head of e.nablaw.in.L.eight.

Under the induction state d.mathcalS.def and the recurrence's shell-width constraint h <= 6 cstar gamma^{-1}, the normalization factor of the fresh shell obeys

  shom_{m-h}^{-2} * h * 3^{2 gamma m}  <=  24 * 3^18 .

The constant is absolute: it depends on neither the dimension nor any model parameter. Only the lower branch of e.shom.h.bounds and the absolute bound cstar <= 3/2 enter.

The fluctuation amplitude

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.rpow_gap_le_gammaPow_mul_spare {d : ℕ} {gamma G : ℝ} (hgamma : 0 < gamma) (hquarter : gamma ≤ 1 / 4) (hd : 2 ≤ d) (hG : 10 ^ 10 * gamma⁻¹ ≤ G) : 3 ^ (-(↑d / 8) * G) ≤ gamma ^ 100 * 3 ^ (-10 ^ 9 * gamma⁻¹)

The Calderon-Zygmund gap factor of e.nablaw.in.L.eight.

For d >= 2, 0 < gamma <= 1/4 and a scale gap G >= 10^10 gamma^{-1} (the manuscript's e.recurrence.params), the decay factor of the middle line of e.nablaw.in.L.eight satisfies

  3^{-(d/8) G}  <=  gamma^100 * 3^{-10^9 / gamma} .

The trailing factor is the room left over for the dimension-only constants: it is the quantitative form of the manuscript's "increasing M in e.cgamma.constraints, if necessary".

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.const_mul_rpow_gap_le_gammaPow {d : ℕ} {C gamma G : ℝ} (hCnonneg : 0 ≤ C) (hgamma : 0 < gamma) (hquarter : gamma ≤ 1 / 4) (hd : 2 ≤ d) (hG : 10 ^ 10 * gamma⁻¹ ≤ G) (hCsmall : C ≤ 3 ^ (10 ^ 9 * gamma⁻¹)) : C * 3 ^ (-(↑d / 8) * G) ≤ gamma ^ 100

The gap factor with a dimension-only prefactor.

The form in which e.nablaw.in.L.eight actually needs the previous estimate: once gamma is small enough that the dimension-only constant C produced by Calderon-Zygmund and by e.km.kn.Lp is below the spare factor 3^(10^9 / gamma), the whole prefactored decay term is below gamma^100.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.exists_gamma_threshold_for_gap_constant (C : ℝ) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ gamma0 ≤ 1 / 4 ∧ ∀ (gamma : ℝ), 0 < gamma → gamma ≤ gamma0 → C ≤ 3 ^ (10 ^ 9 * gamma⁻¹)

"Increasing M in e.cgamma.constraints, if necessary".

For every constant C there is a positive threshold below which the smallness hypothesis of const_mul_rpow_gap_le_gammaPow holds. Together with the previous theorem this makes the manuscript's parenthetical quantitative: no matter which dimension-only constant the Calderon-Zygmund step and e.km.kn.Lp produce, the fluctuation amplitude of e.nablaw.in.L.eight is below gamma^100 once gamma is small.