MultiscaleAbsorption

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

Provider: the final absorption of p.multiscale.estimate

The arithmetic half is the sibling Provider/MultiscaleEstimate/MultiscaleAbsorptionCore.lean.

What is delivered

multiscale_estimate_of_mStarStar (section 10) is the frozen root's statement body (Frozen/Section3/MultiscaleEstimate.lean) verbatim, binder for binder and amplitude spelling for amplitude spelling, with ONE premise inserted:

    mStarStar M < m ->

immediately before inductionState M (m - 1) E. Everything else is unchanged: the same exists Cms, the same window cstar^{-1} eps^{-Cms} <= E, the same smallness cgamma <= (E^{-1})^{10}, the same s in [8 cgamma, 1], ONE (Y, Z) pair for the main conjunct AND the refinement clause, and the two amplitudes

    Cms E s^{-1} sqrt(eps cgamma)   and   Cms eps (s^{-1})^2 exp(-E^{-3} cgamma^{-1}) .

The fit is exact in both directions: the character-for-character copy of the frozen body with the one premise inserted is inhabited by multiscale_estimate_of_mStarStar d itself, and conversely the frozen body implies that premised copy, so no strengthening hides in the endpoint. The two texts differ by mStarStar M < m -> and the proof opener alone. Nothing else about the fit moved: the inserted premise occupies the same slot, and every other binder and amplitude spelling is untouched.

The scale gate on m

The premise inserted above is mStarStar M < m, not the printed m0 in (mstar, infty) cap Z that the display inherits. The endpoint's name multiscale_estimate_of_mStarStar records the gate.

The carried premise (mStarStar M < m) — a named seam, NOT a weakening

Every proved producer of the buckle's five-term display carries the landmark gate mStarStar M < m0:

• Provider.Localization.localization_mathcalE_estimate_ae_unconditional (and its conditional twin localization_mathcalE_estimate_ae);
• exists_badEventSummed_bound, inherited from exists_crude_bound.

Both inherit it from l.shom.continuity, whose own premise it is. The frozen root does not carry it, and neither does the manuscript's Proposition p.multiscale.estimate ("Assume that m in Z and E in [1, infinity) are such that S(m-1, E) is valid"), nor Lemma l.localization.mathcalE. It is not derivable from the frozen root's binders: inductionState M (m-1) E constrains sigmaBar and the error at scales <= m-1 only, and is satisfiable at every m, however far below mStarStar M.

The complementary range is now m <= mStarStar M, and it is proved: the sibling Provider.MultiscaleEstimate.multiscale_estimate_of_le_mStarStar (MultiscaleBaseBranch.lean) proves the same frozen body on exactly that range from the base-case surface.

Gating at mStarStar rather than at mStar removes the band mStarStar M < m <= mStar M, which under an mStar gate is covered by neither branch. That band is a record of what the base-case surface reaches, not an open gap in this chain: the plateau Provider.Base.annealedPlateau_le_mStar states only the diffusivity conjunct nu <= sigmaBar_m <= 2 nu, and disclaims the homogenization-error conjunct; the only proved error statement at m <= mStar (exists_baseCaseMStarErrorConst) fails three ways as a route to this display (deterministic shift literally 2, against an amplitude tending to 0 as E -> infinity; no cgamma factor in (sqrt cstarPlus)^{-1} sqrt(baseLoss d s); s-range Ioo 0 1 excluding s = 1); and the sqrt cgamma gain exists only at the mStarStar (cgamma^3) landmark, while mStarStar M <= mStar M.

Nothing here is weakened: every other binder of the frozen root is consumed as given, and every side condition of every proved producer is discharged from those binders (sections 8--10).

The assembly, in the order it runs

1. Cms (section 8, exists_absorptionConstants) — ParameterWeb.exists_parameterWeb_general at Chom:= max (homogenizationStepConst d) 10^9 with BOTH free slots used: Cwin carries every <= Cms demand and Cshom every <= 2^{Cms} demand, each as a SUM of nonnegative summands. The numeral 10^9 occurs at exactly ONE place in this module, inside the proof of exists_absorbed_envelope, where the enlargement is performed; no statement of either module mentions it.
2. h := waveCutoff (2 max(Chom, 10^9)) eps — one_le_waveCutoff (1 <= h), le_waveCutoff (the corridor), waveCutoff_le_add_one (the bad producer's H-budget), gamma_mul_waveCutoff_le_one (cgamma h <= 1) and three_rpow_five_waveCutoff_le (the 3^{5h} head).
3. The eps^2 normalisation — the whole squared display runs at eps^2, which is what makes the frozen root's refinement clause free: the second conjunct is discharged with its s <= Cms eps hypothesis unused.
4. The localization side — the sibling's localization_mathcalE_estimate_ae_unconditional (the five-term endpoint with BOTH deep Summable premises discharged); the bad lane at ONE Cbad, extracted once from exists_badEventSummed_bound and threaded at Ccg := 2 Cbad, with the carrier bridge ae_sq_cutoffHomogenizationError_eq_homogenizationErrorOnCube_sq.
5. The adjoint leg costs no constant.
6. The buckle — Provider.Orlicz.isTwoTermBigOWithWitnesses_sqrt_of_sq_one_ quarter (Gamma_1 x Gamma_{1/4} on the square becomes Gamma_2 x Gamma_{1/2} on the root), preceded by exists_witnesses_of_envelope (the a.e.-to-pointwise device) and followed by Provider.Orlicz.isTwoTermBigOWithWitnesses_mono_scales.
7. ONE (Y, Z) pair — the witnesses of step 6 serve BOTH conjuncts: the main one after Provider.Orlicz.isTwoTermBigOWithWitnesses_mono_scales, the refinement one from the SAME Gamma_2 component by IsBigOWith.mono_scale. Nothing is re-chosen.

1. The two deep-leg terms

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.twoLaneEnvelope_deepLegA {d : ℕ} [NeZero d] (M : ABKModel d) {m : ℤ} (E : { E : ℝ // 1 ≤ E }) (hE : 15 * (Disorder.cstar M)⁻¹ ≤ ↑E) (hgammaE : M.gamma ≤ (↑E)⁻¹ ^ 10) (hS : Frozen.Section3.inductionState M (m - 1) E) {epsilon : ℝ} (hepsilon : epsilon ∈ Set.Ioc 0 (1 / 2)) (hgate : M.gamma ≤ (homogenizationStepConst d)⁻¹ * (↑E)⁻¹ ^ 2 * epsilon ^ 2) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (h : ℕ) (hcorr : 2 * homogenizationStepConst d * |Real.log epsilon| ≤ ↑h) : TwoLaneEnvelope (↑(Cutoff.cutoffSampleLaw M)) (fun (omega : Cutoff.CutoffSample d) => 12 * (HCPolySupport.Book.Ch02.geometricDiscount s 2 * Localization.gridScaleSeries m s fun (j : ℕ) (R : HCPolySupport.TriadicCube d) => Localization.breakdownLegA R (Cutoff.coefficientCutoffTriadicCoeffFamily M (m - ↑j - ↑h) omega) (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M (m - ↑j - ↑h))))) (96 * homLaneOrdinaryConst d * (s⁻¹ ^ 2 * (epsilon ^ 2 * ↑E ^ 2 * M.gamma))) (96 * homLaneRareConst d * (s⁻¹ ^ 4 * (epsilon ^ 2 * Real.exp (-(2 * (↑E)⁻¹ ^ 3 * M.gamma⁻¹)))))

The primal deep-leg term 12 c_{2s} . Sigma_j 3^{-sj} (avsum_z legA_j^{d/s})^{s/d} of the localization display, at the two lane scales.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.twoLaneEnvelope_deepLegB {d : ℕ} [NeZero d] (M : ABKModel d) {m : ℤ} (E : { E : ℝ // 1 ≤ E }) (hE : 15 * (Disorder.cstar M)⁻¹ ≤ ↑E) (hgammaE : M.gamma ≤ (↑E)⁻¹ ^ 10) (hS : Frozen.Section3.inductionState M (m - 1) E) {epsilon : ℝ} (hepsilon : epsilon ∈ Set.Ioc 0 (1 / 2)) (hgate : M.gamma ≤ (homogenizationStepConst d)⁻¹ * (↑E)⁻¹ ^ 2 * epsilon ^ 2) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) (h : ℕ) (hcorr : 2 * homogenizationStepConst d * |Real.log epsilon| ≤ ↑h) : TwoLaneEnvelope (↑(Cutoff.cutoffSampleLaw M)) (fun (omega : Cutoff.CutoffSample d) => 12 * (HCPolySupport.Book.Ch02.geometricDiscount s 2 * Localization.gridScaleSeries m s fun (j : ℕ) (R : HCPolySupport.TriadicCube d) => Localization.breakdownLegB R (Cutoff.coefficientCutoffTriadicCoeffFamily M (m - ↑j - ↑h) omega) (Observable.isotropicComparatorMatrix (Annealed.sigmaBar M (m - ↑j - ↑h))))) (96 * homLaneOrdinaryConst d * (s⁻¹ ^ 2 * (epsilon ^ 2 * ↑E ^ 2 * M.gamma))) (96 * homLaneRareConst d * (s⁻¹ ^ 4 * (epsilon ^ 2 * Real.exp (-(2 * (↑E)⁻¹ ^ 3 * M.gamma⁻¹)))))

The adjoint deep-leg term, at the same two lane scales. The (J3) negation is a law isomorphism, so the adjoint leg costs no constant: its envelope is the primal envelope read at the negated sample.

2. The wave term

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.twoLaneEnvelope_waveTerm {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) {s : ℝ} (hs : 0 < s) {Cinj Awave : ℝ} (hCinj : 0 ≤ Cinj) (hbound : HCPolySupport.IndependentSums.IsBigOWith (↑M.P) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.ShellSeq d) => waveSizesTotalW2 M m h s omega) Awave) : TwoLaneEnvelope (↑(Cutoff.cutoffSampleLaw M)) (fun (omega : Cutoff.CutoffSample d) => Cinj * waveSizesTotalW2 M m h s ↑omega) (Cinj * Awave) (Cinj * 0)

The wave term 32 Cinj cstar^{-1} cgamma . waveSizesTotalW2, at the Gamma_1 scale of e.wave.sizes and an empty rare lane.

3. The bad-event term

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.twoLaneEnvelope_badTerm {d : ℕ} (M : ABKModel d) (m : ℤ) {s : ℝ} (hs4 : 0 < s / 4) {W G : Cutoff.CutoffSample d → ℝ} {B1 B2 : ℝ} (hGeq : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), G omega = Observable.cutoffHomogenizationError M m ⟨s / 4, hs4⟩ omega ^ 2) (hbad : Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (2 / 7)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffHomogenizationError M m ⟨s / 4, hs4⟩ omega ^ 2 * W omega) B1 B2) : TwoLaneEnvelope (↑(Cutoff.cutoffSampleLaw M)) (fun (omega : Cutoff.CutoffSample d) => 8 * W omega * G omega) (8 * B1) (8 * B2)

The bad-event term 8 . max_l 3^{-s(m-l)/2}(avsum_z 1_{not Q})^{s/d} . E^2_{s/4} of the localization display.

Two things happen here and nothing else. The proved producer exists_badEventSummed_bound states the display at the Gamma_{2/7} rare profile of e.local.bad.events.summed; the squared display of the buckle runs at Gamma_{1/4}, and 2/7 > 1/4, so the index is lowered — never raised — by Provider.Orlicz.isTwoTermBigOWith_mono_exponent. And the producer's left factor is the Section 3 observable E_{s/4}^2 while the localization display's is CoarseGraining's HomogenizationErrorOnCube; the two agree almost surely, which is the hypothesis hGeq (its producer is the proved BadEventSummed.ae_sq_cutoffHomogenizationError_eq_homogenizationErrorOnCube_sq).

4--6. (moved) The three scale bridges of the non-lane terms, the bad

lane's two amplitudes, and the deterministic remainder now live in the sibling Provider/MultiscaleEstimate/MultiscaleAbsorptionArith.lean, split out at the 1500-line file cap, with their section headers, statements and proof text unchanged. Their section numbers are kept there so that every cross-reference in this header still points where it did; the four consumed below are MultiscaleAbsorptionArith.polyTerm_le_ordinaryScale, .badOrdinaryAmplitude_le, .badRareAmplitude_le and .remainderTerm_le.

7. The five-term sum in the two normal forms

8. The parameter web at the assembled constants

9. The absorbed envelope of the squared display

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.exists_absorbed_envelope (d : ℕ) [NeZero d] : ∃ (Cms : ℝ) (Ktot : ℝ) (Ltot : ℝ), 0 < Cms ∧ 4 ≤ Cms ∧ 0 < Ktot ∧ 0 < Ltot ∧ √Ktot ≤ Cms ∧ √Ltot ≤ Cms ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), mStarStar M < m → Frozen.Section3.inductionState M (m - 1) E → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), (Disorder.cstar M)⁻¹ * epsilon ^ (-Cms) ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), TwoLaneEnvelope (↑(Cutoff.cutoffSampleLaw M)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffHomogenizationError M m ⟨s, ⋯⟩ omega ^ 2) (Ktot * (s⁻¹ ^ 2 * (epsilon ^ 2 * ↑E ^ 2 * M.gamma))) (Ltot * (s⁻¹ ^ 4 * (epsilon ^ 2 * Real.exp (-(2 * (↑E)⁻¹ ^ 3 * M.gamma⁻¹)))))

The final absorption. At the Cms of section 8, the whole five-term localization display collapses onto the squared display's two normal forms

    A1 = Ktot . (s^{-1})^2 (eps^2 E^2 cgamma) ,
    A2 = Ltot . (s^{-1})^4 (eps^2 exp(-2 E^{-3} cgamma^{-1})) .

The single premise beyond the frozen root's own binders is mStarStar M < m ( option (i)); see the module header.

10. The buckle, and p.multiscale.estimate on the carried premise

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.multiscale_estimate_of_mStarStar (d : ℕ) : ∃ (Cms : ℝ), 0 < Cms ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), mStarStar M < m → Frozen.Section3.inductionState M (m - 1) E → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), (Disorder.cstar M)⁻¹ * epsilon ^ (-Cms) ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), ∃ (Y : Cutoff.CutoffSample d → ℝ) (Z : Cutoff.CutoffSample d → ℝ), Probability.IsTwoTermBigOWithWitnesses (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M m ⟨s, ⋯⟩) Y Z (Cms * ↑E * s⁻¹ * √(epsilon * M.gamma)) (Cms * epsilon * s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹))) ∧ (s ≤ Cms * epsilon → HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) Y (Cms * epsilon * ↑E * s⁻¹ * √M.gamma))

The endpoint for p.multiscale.estimate — the frozen root's statement body verbatim (Frozen/Section3/MultiscaleEstimate.lean), with the one carried premise mStarStar M < m inserted immediately before the induction state; the name records the gate.

That premise is not a weakening of the mathematics: it is the landmark gate of l.shom.continuity, inherited verbatim by BOTH of the buckle's proved inputs (Provider.Localization.localization_mathcalE_estimate_ae_unconditional and exists_badEventSummed_bound), and the frozen root — like the manuscript's Proposition p.multiscale.estimate — carries no such binder. The complementary branch is now m <= mStarStar M, and it is proved as multiscale_estimate_of_le_mStarStar (MultiscaleBaseBranch.lean); nothing in this module supplies it, and no proved producer of the display is free of the gate. See the module header, "The scale gate on m" and "The carried premise".

Everything else is the frozen root, binder for binder and amplitude spelling for amplitude spelling: one (Y, Z) pair serves both the main conjunct and the refinement clause, and the refinement clause is discharged unconditionally -- its s <= Cms eps hypothesis is consumed by nothing.