StepSevenSigmaBarChain

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

t.regularity Step 7d: the narrowed chain, generic in the σ comparison

What this module does

The fifth and last of the sites where the proved chain hard-codes the printed σ_{n'} ≤ 2 σ_m is the narrowed Step-7d chain.

Making the comparison constant a parameter closes the hcomp gap: the σ comparison can then be discharged from the frozen Section-3 inductionState by sigmaBar_le_four_mul_sigmaBar, so the chain no longer asks its caller for a comparison it cannot supply. The output constant picks up √4 = 2 where print writes √2.

References

• ABK26, Step 7d; e.energy.density.estimate.

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenEnd_chain_of_lambda_gen (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ {alpha : ℝ} {n m : ℤ} {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (u : HCPolySupport.Book.Ch03.ForcedCubeSolution Q a g) {Cg Cmean Clam Ccmp Kg Kd Ks Ctr shomNp shomMp shomM gradLoc oscTrunc gradM dataG dataM W G H : ℝ}, 0 ≤ Cg → 0 ≤ Cmean → 0 ≤ Clam → 0 ≤ Ks → 0 ≤ Ccmp → 0 ≤ shomMp → 0 < shomM → 0 ≤ oscTrunc → 0 ≤ gradM → 0 ≤ dataG → 0 ≤ W → 0 ≤ G → 0 ≤ H → HCPolySupport.Book.Ch03.ForceBesovRegularity Q stepSevenCgS g → stepSevenCgLamInv Q a stepSevenCgS ≤ Clam * shomMp → HCPolySupport.Book.Ch03.forcedSolutionEnergyNorm Q a u ≤ Kg * gradM → HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q stepSevenCgS g ≤ Kd * dataG → shomMp ≤ Ks * shomM⁻¹ → √Ks * Kg ≤ Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) → Ks * Kd ≤ Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) → oscTrunc ≤ Cmean * ((HCPolySupport.cubeScaleFactor Q)⁻¹ * HCPolySupport.cubeBesovOscillation Q 2 fun (x : HCPolySupport.Vec d) => u.toH1.toFun x) → shomNp ≤ Ccmp * shomM → 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) → gradLoc ≤ Cg * √Ccmp * (Cmean * stepSevenEmbeddingConst d * stepSevenBridgeConst stepSevenCgS * (C * 64 * (√Clam + Clam)) * 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)

Step 7d, end to end, with hcg/hembed/hbridge discharged and the σ comparison generic.

The narrowed Step-7d chain with the printed constant 2 replaced by a parameter Ccmp; the remaining conditional inputs are still exactly hlambda (e.lambda.stability.applied) and the Step-7c gradient display hgrad.