ShomContinuity

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

Continuity of m |-> shom_m: two-sided ratio control across scales

ABK26, l.shom.continuity and its proof; the consuming display e.switchtheshoms.betterer.again of the localization shom-switch.

What is delivered

For the genuine running diffusivity Annealed.sigmaBar on the Section 3 carriers, on the premise list of l.shom.continuity --- mstarstar < m0 (the correction of the printed mstar < m0; see the dedicated section below), the induction state S(m0-1,E), E >= C cstar^{-1} and cgamma <= E^{-10} --- and for every pair of integer scales n <= m <= m0:

1. the quarter comparison shom_m >= (1/4) shom_n, and its ratio form shom_n shom_m^{-1} <= 4, which is the honest constant of the switch step's quoted shom_m^{-1} shom_{l-h} <= 2;
2. the growth cap shom_m <= 4 . 3^{cgamma (m-n)} shom_n;
3. its short-range collapse shom_m shom_n^{-1} <= 12 whenever cgamma (m-n) <= 1 (the printed 3^{cgamma h} <= 3 step);
4. the two-sided defect display e.shom.m.vs.shom.n, at the printed second entry of the minimum,

  |shom_m shom_n^{-1} - 1| + |shom_n shom_m^{-1} - 1|
      <= C . min{1, cgamma (m-n) + E^2 cgamma |log cgamma|^2} . 3^{cgamma (m-n)} .

The route: the three-branch split

The display is proved by one case split on the size of the min-entry and, inside the small branch, one dichotomy against the flow's relative defect delta := Cflow cstar^{-1} E cgamma^{1/2} |log cgamma|. Write x := cgamma (m-n) and Es := E^2 cgamma |log cgamma|^2.

• (A) far, x + Es >= 1/8: ShomContinuityCore.ratioSum_le_of_twoSided gives <= 8 . 3^{x} outright from the two-sided envelope, and min{1, x+Es} >= 1/8 absorbs the constant. No regime input is used.
• (B) flow, x + Es < 1/8 and delta <= x: the diffusivity asymptotics pin both shom_m and shom_n to the same profile at relative accuracy delta, and the profile itself grows by 1 + 4x across the gap, so the two ratio defects sum to at most 8x + 24 delta <= 32 x.
• (C) recurrence, x + Es < 1/8 and x < delta: the sharpened cgamma-gate E^4 cgamma^{1/2} |log cgamma| <= 16 (proved below with integer powers only, out of |log g| <= 16 g^{-1/16} and cgamma <= E^{-10}) forces delta <= cstar^2 / 2, hence x <= cstar --- the pair (n, m) is inside the recurrence producer's window m <= n + cstar cgamma^{-1}.

Branch (C) is where the printed entry is produced; branches (A) and (B) never see it. The manuscript's medium band (1/2)min{1,cstar^2} cgamma^{-1} <= m-n <= cgamma^{-1} disappears under the sharpened gate ---, which records that the printed C = C(d) is not attainable from the quoted input alone but is attainable after the sharpening.

The scale gate on m0 (-bin statement change)

The landmark premise carried below is mStarStar M < m0, not the printed m0 in (mstar, infty) cap Z. The two producers consumed below are already stated at the corrected gate, so the change here is the single binder and nothing else: the proof forwards the premise to them verbatim.

Inputs consumed, never re-proved

• Closure.diffusivity_asymptotics_proved --- the provider export of the Algsuperdiff.Frozen.Section3.diffusivity_asymptotics: the shom flow display at every m <= m0 together with the two-sided envelope at the top scale m0, gated at the mStarStar M < m0. (The frozen root itself is consumed through this export, the frozen roots being outside the default build target.)
• Closure.recurrenceIntegrationBinders_of_twoSidedClosure, and through it Closure.NodeContract.integrationHypotheses_of_displays (NodeContract.lean), Closure.TwoSidedTargets.sigmaBar_le_of_upperDisplay (TwoSidedTargets.lean) and Closure.TwoSidedTargets.sigmaBar_ge_of_displays (TwoSidedTargets.lean), the three conversions that turn the two printed displays of e.what.do.we.have into the integration binders; the closure contract itself is discharged as described above.
• ApproximateRecurrence.recurrence_binders_of_below_landmark and its inputs Diffusivity.annealedPlateau_smallScaleBound (e.plateau.region.bound), Provider.Scales.le_mStarStar_iff_rpow_le (e.mstarstar), Provider.Disorder.cstar_le_three_halves and ApproximateRecurrence.cstar_le_cstarPlus.
• Diffusivity.ShomContinuityCore --- the model-free arithmetic core: the comparator diffMax, its positivity and geometric growth, the quarter comparison quarter_le_of_twoSided, and the far branch ratioSum_le_of_twoSided at the explicit constant 8. That file explicitly disclaims realizing the node because the short-range branch needs more than the envelope; this file supplies the rest.
• RecurrenceIntegration.Internal.recurrenceIncrement_le_count and recurrenceIncrement_nonneg --- the two elementary facts about A_{n,m} used in branch (C).
• Localization.ShomContinuityArithmetic --- this route's own model-free arithmetic layer, twenty-three protected theorems over abstract reals. The five model-level lemmas of the route (near_flow_bound, near_recurrence_bound, window_binders, slack_bounds, defect_display) stayed here and remain private.

References

• ABK26, l.shom.continuity; proof.
• ABK26, e.shom.h.bounds; d.mathcalS.def.
• ABK26, e.what.do.we.have; l.approximate.recurrence.formula.
• ABK26, l.integrate.approx.recurrence; e.mstarstar; p.base.case.
• ABK26, the localization shom-switch.

Branches (B) and (C) on the Section 3 carriers

Branch (C) on the Section 3 carriers

The two producers, stitched over the whole window

The defect display: the three-branch dispatch

The node's arithmetic on the Section 3 carriers

theorem Algsuperdiff.Section3.Provider.Localization.shom_continuity (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), mStarStar M < m0 → Frozen.Section3.inductionState M (m0 - 1) E → C * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → ∀ (m n : ℤ), n ≤ m → m ≤ m0 → 1 / 4 * ↑(Annealed.sigmaBar M n) ≤ ↑(Annealed.sigmaBar M m) ∧ ↑(Annealed.sigmaBar M n) * (↑(Annealed.sigmaBar M m))⁻¹ ≤ 4 ∧ ↑(Annealed.sigmaBar M m) ≤ 4 * 3 ^ (M.gamma * (↑m - ↑n)) * ↑(Annealed.sigmaBar M n) ∧ (M.gamma * (↑m - ↑n) ≤ 1 → ↑(Annealed.sigmaBar M m) * (↑(Annealed.sigmaBar M n))⁻¹ ≤ 12) ∧ |↑(Annealed.sigmaBar M m) * (↑(Annealed.sigmaBar M n))⁻¹ - 1| + |↑(Annealed.sigmaBar M n) * (↑(Annealed.sigmaBar M m))⁻¹ - 1| ≤ C * min 1 (M.gamma * (↑m - ↑n) + ↑E ^ 2 * (M.gamma * |Real.log M.gamma| ^ 2)) * 3 ^ (M.gamma * (↑m - ↑n))

Continuity of m |-> shom_m (l.shom.continuity, ABK26), on the printed premise list with the landmark gate at mStarStar M < m0, for every pair of integer scales n <= m <= m0.

Proved from Closure.diffusivity_asymptotics_proved and Closure.recurrenceIntegrationBinders_of_twoSidedClosure together with the closure contract's two produced obligations (closureInteriorBesovEnvelopeInput_proved, closureStripRemainder_proved), and the below-landmark binder producer ApproximateRecurrence.recurrence_binders_of_below_landmark.