Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Regularity.StepSevenSigmaBar

StepSevenSigmaBar #

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

t.regularity Step 7d: the σ comparison at a generic constant #

The gap this module closes #

The Step-7d chain hard-codes the printed comparison

  e.shom.m.vs.shom.n :   σ_{n'}  ≤  2 σ_m

at the literal constant 2 in five places along the Step-7d chain — the data-leg merge, the merged and the pinned energy-density estimates, the end chain and its narrowed form — while the only comparison proved here is Annular.SigmaBarBudget.sigmaBar_ratio_le_four, i.e. the constant 4.

The route is the generic-constant collapse pattern already used for Ccol: generic-Ccmp siblings of the pinned theorems, leaving the pinned statements untouched.

The printed √2 becomes √Ccmp; at Ccmp = 4 that is 2. The difference is immaterial inside C(d, c_*) — the deviation that StepSevenEndAssembly's docstring already describes.

What sigmaBar_ratio_le_four actually gives #

Annular.sigmaBar_ratio_le_four M hS (hnm : n - 2 ≤ m) (hm : m ≤ m0) reads σ_m^{-1}·σ_{n-2} ≤ 4. Re-indexed at n := n' + 2 it is exactly σ_{n'} ≤ 4 σ_m under n' ≤ m ≤ m₀ — no adjacency and no plateau hypothesis.

References #

1. The proved comparison, in the chain's own slot shape #

source
theorem Algsuperdiff.Section4.Provider.Regularity.sigmaBar_le_four_mul_sigmaBar {d : ℕ} (M : Section3.ABKModel d) {m0 : ℤ} {Ecap : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 Ecap) {n' m : ℤ} (hnm : n' ≤ m) (hm : m ≤ m0) :
↑(Section3.Annealed.sigmaBar M n') ≤ 4 * ↑(Section3.Annealed.sigmaBar M m)

e.shom.m.vs.shom.n at the proved constant 4.

Annular.sigmaBar_ratio_le_four in the multiplicative form the Step-7d chain consumes:

  σ_{n'}  ≤  4 σ_m          for  n' ≤ m ≤ m₀ .

Derived from conjunct 1 of the frozen Section-3 inductionState at the two scales alone — no adjacency.

2. The data-leg collapse, generic in Ccmp #

source
theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenDataLeg_merge_gen {shomNp shomM Ccmp W G H : ℝ} (hshomM : 0 < shomM) (hCcmp : 0 ≤ Ccmp) (hW : 0 ≤ W) (hG : 0 ≤ G) (hH : 0 ≤ H) (hcomp : shomNp ≤ Ccmp * shomM) :
√shomNp * (W * (shomM⁻¹ * G + H)) ≤ √Ccmp * (W * ((√shomM)⁻¹ * G + √shomM * H))

The data-leg merge at a generic comparison constant.

  √σ_{n'} · W · (σ_m^{-1}G + H)  ≤  √Ccmp · W · ((√σ_m)^{-1}G + √σ_m·H) .

At Ccmp := 2 this is the printed data-leg merge verbatim (machine-checked); at Ccmp := 4 it is the proved envelope's own comparison, at cost 2.

3. e.energy.density.estimate with the printed bracket, generic in Ccmp #

source
theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenEnergyDensityEstimate_merged_gen {Cg Cend Ccmp R34 R14 shomNp shomM gradLoc oscTrunc dataM gradM dataG W G H : ℝ} (hCg : 0 ≤ Cg) (hCcmp : 0 ≤ Ccmp) (hshomM : 0 < shomM) (hR34 : 0 ≤ R34) (hoscTrunc : 0 ≤ oscTrunc) (hW : 0 ≤ W) (hG : 0 ≤ G) (hH : 0 ≤ H) (hcomp : shomNp ≤ Ccmp * shomM) (hgrad : gradLoc ≤ Cg * √shomNp * R34 * oscTrunc + Cg * R34 * (√shomNp * (W * (shomM⁻¹ * G + H)) + dataM)) (hend : oscTrunc ≤ Cend * R14 * (√shomM⁻¹ * (gradM + √shomM⁻¹ * dataG))) :
gradLoc ≤ Cg * (√Ccmp * (Cend * R14)) * R34 * (gradM + √shomM⁻¹ * dataG) + Cg * R34 * (√Ccmp * (W * ((√shomM)⁻¹ * G + √shomM * H)) + dataM)

The merged energy-density estimate at a generic comparison constant.

stepSevenEnergyDensityEstimate_compose (already generic in Ccmp) followed by stepSevenDataLeg_merge_gen at the SAME comparison, so e.shom.m.vs.shom.n is still consumed exactly once. At Ccmp := 2 this is the pinned parent verbatim.

source
theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenEnergyDensityEstimate_gen {alpha : ℝ} {n m : ℤ} {Cg Cend Ccmp shomNp shomM gradLoc oscTrunc dataM gradM dataG W G H : ℝ} (hCg : 0 ≤ Cg) (hCcmp : 0 ≤ Ccmp) (hshomM : 0 < shomM) (hoscTrunc : 0 ≤ oscTrunc) (hW : 0 ≤ W) (hG : 0 ≤ G) (hH : 0 ≤ H) (hcomp : shomNp ≤ Ccmp * shomM) (hgrad : gradLoc ≤ Cg * √shomNp * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * oscTrunc + Cg * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√shomNp * (W * (shomM⁻¹ * G + H)) + dataM)) (hend : oscTrunc ≤ Cend * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) * (√shomM⁻¹ * (gradM + √shomM⁻¹ * dataG))) :
gradLoc ≤ Cg * √Ccmp * Cend * Real.rpow 3 (stepSixExponent alpha n m) * (gradM + √shomM⁻¹ * dataG) + Cg * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√Ccmp * (W * ((√shomM)⁻¹ * G + √shomM * H)) + dataM)

The energy-density estimate at a generic comparison constant, i.e. e.energy.density.estimate at the printed exponent 3^{(1-α)(m-n)} with the printed data bracket and the σ comparison left as a parameter. At Ccmp:= 2 this is the pinned parent verbatim.

4. Step 7d end to end, generic in Ccmp #

source
theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenEnd_chain_gen {alpha : ℝ} {n m : ℤ} {Cg Cmean Cemb Cbr Cout Ctr Ccmp shomNp shomM gradLoc oscTrunc oscLoc besovP1 besov dataM gradM dataG W G H : ℝ} (hCg : 0 ≤ Cg) (hCmean : 0 ≤ Cmean) (hCemb : 0 ≤ Cemb) (hCbr : 0 ≤ Cbr) (hCcmp : 0 ≤ Ccmp) (hshomM : 0 < shomM) (hoscTrunc : 0 ≤ oscTrunc) (hW : 0 ≤ W) (hG : 0 ≤ G) (hH : 0 ≤ H) (hcomp : shomNp ≤ Ccmp * shomM) (hgrad : gradLoc ≤ Cg * √shomNp * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * oscTrunc + Cg * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√shomNp * (W * (shomM⁻¹ * G + H)) + dataM)) (hmean : oscTrunc ≤ Cmean * oscLoc) (hembed : oscLoc ≤ Cemb * besovP1) (hbridge : besovP1 ≤ Cbr * besov) (hpoincare : besov ≤ Cout * (Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m)) * (√shomM⁻¹ * gradM + shomM⁻¹ * dataG)) :
gradLoc ≤ Cg * √Ccmp * (Cmean * Cemb * Cbr * Cout * Ctr) * Real.rpow 3 (stepSixExponent alpha n m) * (gradM + √shomM⁻¹ * dataG) + Cg * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√Ccmp * (W * ((√shomM)⁻¹ * G + √shomM * H)) + dataM)

The Step-7d end chain at a generic comparison constant.

The three proved displays of the node, chained, with e.shom.m.vs.shom.n a parameter rather than the printed 2. Each hypothesis is literally the conclusion of the named theorem, exactly as in the pinned parent, and at Ccmp:= 2 the statement IS the pinned parent.