GammaTenStripRemainder

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

The boundary-strip residual of the interior route, assembled

ABK26, Step 2 of l.approximate.recurrence.formula, target e.lower.bound.localization.terms.

What this module is

Closure.ClosureInteriorSplit.ClosureStripRemainder d is the second of the two conditional A obligations of the interior route. Written out, it asks: at every model, window, gap and pair of directions --- with no regime, no direction normalization and no gap positivity --- for all large localization cubes there is a bound Cstrip on the full-mesh average of the squared cell expectations of the Step-2 integrand, which the signed Cauchy--Schwarz gate sqrt(d 3^{g-p}) sqrt(Cstrip) <= cgamma^{10}/2 absorbs.

This module assembles it from two pathwise inputs and the polynomial rate of Closure.GammaTenStripLambdaGrowth. The assembly is where the two competing rates are compared: the strip constant grows polynomially in the localization scale K (degree eight, through the ellipticity moment), while the mesh depth p = closureMeshDepth M n h K grows linearly, so the gate's 3^{g-p} decays geometrically. eventually_poly_le_geometric closes it.

What is proved

• cubeFamilyAverage_integral_sq_stripCellPotentialDatum_le_of_majorant and its flux mirror --- the two grid binders hpot, hflux of Closure.GammaTenStripBound.gammaTenStrip_cell_average_sq_le, produced from a pathwise majorant G of the shifted fourth energy on the localization cube rather than from an integrability statement about that fourth energy itself. The route is Closure.GammaTenStripEnergy's pathwise fold cubeFamilyAverage_sq_cubeAverage_vecNormSq_le_originCubeFourthEnergy composed with LocalizationFluctuationGridEighth.cubeFamilyAverage_integral_le_of_pointwise.
• closureStripRemainder_of_majorant --- ClosureStripRemainder d from the two inputs, with the gate discharged ∀ᶠ K.
• closureStripRemainder_proved and diffusivity_asymptotics_proved --- the two endpoints of this module: ClosureStripRemainder d and the frozen statement's conclusion, each from (d : ℕ) [NeZero d] (hd : 2 ≤ d) alone; every other input above is discharged internally.

Binders

closureStripRemainder_of_majorant carries hd : 2 <= d and the two Prop binders hmaj (the pathwise fourth-energy majorant with a localization-scale free expectation bound) and hsqD/hsqF (the sample second moments of the two cell data). It carries no regime, no inductionState, no cgamma smallness and no normalization of e, e'; the obligation it proves has none either.

Scope

Internal Provider infrastructure. The intermediate declarations are a conditional A route for Closure.ClosureInteriorSplit.ClosureStripRemainder; the two endpoints closureStripRemainder_proved and diffusivity_asymptotics_proved carry no conditional binder beyond (d: ℕ) [NeZero d] (2 ≤ d). There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

The scale gate on m0 (-bin statement change)

diffusivity_asymptotics_proved gates m0 at mStarStar M < m0, not at the printed m0 in (mstar, infty) cap Z.

References

• ABK26, l.approximate.recurrence.formula Step 2.

The two grid binders from a pathwise majorant

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_integral_sq_stripCellPotentialDatum_le_of_majorant {d : ℕ} [NeZero d] (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K j : ℕ) (e e' : HCPolySupport.Vec d) (hDsq : ∀ R ∈ mesoCubeGrid d (↑K) (↑K - ↑j), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => stripCellPotentialDatum M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega ^ 2) ↑(Cutoff.cutoffSampleLaw M)) {G : Cutoff.CutoffSample d → ℝ} (hGint : MeasureTheory.Integrable G ↑(Cutoff.cutoffSampleLaw M)) (hGD : ∀ (omega : Cutoff.CutoffSample d), (originCubeFourthEnergy ↑K fun (x : HCPolySupport.Vec d) => e' + (closureDirichletAlong M n h K e ↑omega).grad x) ≤ G omega) : (cubeFamilyAverage (mesoCubeGrid d (↑K) (↑K - ↑j)) fun (R : HCPolySupport.TriadicCube d) => ∫ (omega : Cutoff.CutoffSample d), stripCellPotentialDatum M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega ^ 2 ∂↑(Cutoff.cutoffSampleLaw M)) ≤ 4 * (↑(Annealed.sigmaBar M n))⁻¹ ^ 2 * ∫ (omega : Cutoff.CutoffSample d), G omega ∂↑(Cutoff.cutoffSampleLaw M)

hpot from a pathwise majorant of the shifted fourth energy.

on the cell second moments hDsq, on the sample integrability of the majorant G and on its pathwise domination hGD. No measurability of the fourth energy itself is used.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_integral_sq_stripCellFluxDatum_le_of_majorant {d : ℕ} [NeZero d] (hd : 2 ≤ d) (M : ABKModel d) (n : ℤ) (h K j : ℕ) (e e' : HCPolySupport.Vec d) (hFsq : ∀ R ∈ mesoCubeGrid d (↑K) (↑K - ↑j), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => stripCellFluxDatum M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega ^ 2) ↑(Cutoff.cutoffSampleLaw M)) {G : Cutoff.CutoffSample d → ℝ} (hGint : MeasureTheory.Integrable G ↑(Cutoff.cutoffSampleLaw M)) (hGN : ∀ (omega : Cutoff.CutoffSample d), (originCubeFourthEnergy ↑K fun (x : HCPolySupport.Vec d) => e + neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega) x) ≤ G omega) : (cubeFamilyAverage (mesoCubeGrid d (↑K) (↑K - ↑j)) fun (R : HCPolySupport.TriadicCube d) => ∫ (omega : Cutoff.CutoffSample d), stripCellFluxDatum M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega ^ 2 ∂↑(Cutoff.cutoffSampleLaw M)) ≤ 4 * ↑(Annealed.sigmaBar M n) ^ 2 * ∫ (omega : Cutoff.CutoffSample d), G omega ∂↑(Cutoff.cutoffSampleLaw M)

hflux from a pathwise majorant of the shifted fourth energy.

exactly as its potential mirror.

The obligation

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureStripRemainder_of_majorant (d : ℕ) [NeZero d] (hd : 2 ≤ d) (hmaj : ∀ (M : ABKModel d) (n : ℤ) (h : ℕ) (e e' : HCPolySupport.Vec d), ∃ (B : ℝ), 0 ≤ B ∧ ∀ (K : ℕ), n + ↑h ≤ ↑K → ∃ (G : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d), 0 ≤ G omega) ∧ MeasureTheory.Integrable G ↑(Cutoff.cutoffSampleLaw M) ∧ ∫ (omega : Cutoff.CutoffSample d), G omega ∂↑(Cutoff.cutoffSampleLaw M) ≤ B ∧ (∀ (omega : Cutoff.CutoffSample d), (originCubeFourthEnergy ↑K fun (x : HCPolySupport.Vec d) => e' + (closureDirichletAlong M n h K e ↑omega).grad x) ≤ G omega) ∧ ∀ (omega : Cutoff.CutoffSample d), (originCubeFourthEnergy ↑K fun (x : HCPolySupport.Vec d) => e + neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega) x) ≤ G omega) (hsqD : ∀ (M : ABKModel d) (n : ℤ) (h K : ℕ) (e e' : HCPolySupport.Vec d) (jd : ℕ), ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) jd, ∀ (G : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d), 0 ≤ G omega) → MeasureTheory.Integrable G ↑(Cutoff.cutoffSampleLaw M) → (∀ (omega : Cutoff.CutoffSample d), (originCubeFourthEnergy ↑K fun (x : HCPolySupport.Vec d) => e' + (closureDirichletAlong M n h K e ↑omega).grad x) ≤ G omega) → MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => stripCellPotentialDatum M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega ^ 2) ↑(Cutoff.cutoffSampleLaw M)) (hsqF : ∀ (M : ABKModel d) (n : ℤ) (h K : ℕ) (e e' : HCPolySupport.Vec d) (jd : ℕ), ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) jd, ∀ (G : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d), 0 ≤ G omega) → MeasureTheory.Integrable G ↑(Cutoff.cutoffSampleLaw M) → (∀ (omega : Cutoff.CutoffSample d), (originCubeFourthEnergy ↑K fun (x : HCPolySupport.Vec d) => e + neumannFluxField (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' (closureNeumannAlong M n h K e' ↑omega) x) ≤ G omega) → MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => stripCellFluxDatum M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega ^ 2) ↑(Cutoff.cutoffSampleLaw M)) : ClosureStripRemainder d

Closure.ClosureInteriorSplit.ClosureStripRemainder d from the pathwise majorant and the two cell second moments.

The strip constant is Closure.GammaTenStripBound.gammaTenStripConst at the two grid moments produced above. Its only localization-scale dependence is the ellipticity moment, which Closure.GammaTenStripLambdaGrowth bounds by a degree-eight polynomial in K; the gate's 3^{g-p} decays geometrically in K because p = closureMeshDepth M n h K is eventually K - recurrenceMesoScale. eventually_poly_le_geometric compares the two rates.

on hd, hmaj, hsqD, hsqF and nothing else: no regime, no inductionState, no cgamma smallness, no normalization of e, e' and no positivity of h.

The obligation, unconditionally

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureStripRemainder_proved (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ClosureStripRemainder d

Closure.ClosureInteriorSplit.ClosureStripRemainder d.

The two Prop binders of closureStripRemainder_of_majorant are discharged by Closure.GammaTenStripPathwise.exists_strip_fourthEnergy_majorant and by the two cell second moments of Closure.GammaTenStripCellSquare. Only d, [NeZero d] and hd : 2 <= d survive.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.diffusivity_asymptotics_proved (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ∃ (Cflow : ℝ), 0 < Cflow ∧ ∀ (M : ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }), mStarStar M < m0 → Frozen.Section3.inductionState M (m0 - 1) E → Cflow * (Disorder.cstar M)⁻¹ ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → (∀ m ≤ m0, |↑(Annealed.sigmaBar M m) - √(M.nu ^ 2 + Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m))| ≤ Cflow * (Disorder.cstar M)⁻¹ * ↑E * √M.gamma * |Real.log M.gamma| * ↑(Annealed.sigmaBar M m)) ∧ 1 / 4 * max (Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m0)) (M.nu ^ 2) ≤ ↑(Annealed.sigmaBar M m0) ^ 2 ∧ ↑(Annealed.sigmaBar M m0) ^ 2 ≤ 4 * max (Disorder.cstar M * M.gamma⁻¹ * 3 ^ (2 * M.gamma * ↑m0)) (M.nu ^ 2)

The diffusivity asymptotics.

The proof consumes the two produced obligations of Closure.ClosureInteriorSplit: the interior-mesh Besov envelope (Closure.GammaTenInteriorHosc.closureInteriorBesovEnvelopeInput_proved) and the boundary-strip residual (closureStripRemainder_proved).

Binder note: the frozen statement's binder list is (d : ℕ) alone; this composition additionally carries [NeZero d] and hd : 2 <= d, which come from Closure.ClosureTerminalStrip.diffusivity_asymptotics_of_strip and are not derivable from d : ℕ.