SplitObligationsRegime

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

Obligation (1) of SplitScaleObligations, at the closure's own families

ABK26, l.approximate.recurrence.formula, Steps 1--3, e.recurrence.params.

What this module supplies

Two things.

• gamma_le_of_closureRegime --- the standing translation of the manuscript's parameter block into a cgamma-threshold. This is the same projection the proved PrincipalResponseTerminal performs; it is reproved here because it is private there.

• exists_const_eventually_integrable_switchCubeEnergy_closureFamilies --- the first conjunct of Closure.SplitProducerFold.SplitScaleObligations, at the closure's own corrector families, for all sufficiently large localization cubes, inside Closure.ClosureRegime.

The per-cell content is Closure.SplitObligationsPrincipal.integrable_switchCubeEnergy_of_integrable_switchEllipLoad_sq, fed by the proved PrincipalResponseGoodEnergy.exists_gamma0_integrable_switchEllipLoad_principalPz_sq transported from M.P to Cutoff.cutoffSampleLaw M along the measurable embedding of Cutoff.map_cutoffSampleLaw_val, and by the proved measurability Closure.SplitProducerLoad.measurable_meshCellLoad.

Binders

Exactly Closure.ClosureRegime at the named threshold and the two direction bounds |e| <= 1, |e'| <= 1. The large-cube gate and the depth-naming identity are produced internally as eventual statements in K. Nothing else is assumed; in particular no measurability, moment or selection property of the corrector families occurs as a binder.

Scope

There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula, Steps 1--3, e.recurrence.params, e.Pz.def.

The cgamma-threshold carried by the regime

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gamma_le_of_closureRegime {d : ℕ} {C g : ℝ} {M : ABKModel d} {n : ℤ} {h : ℕ} {Ec : { E : ℝ // 1 ≤ E }} (hg : 0 < g) (hC : 3 / 2 * g⁻¹ ≤ C) (hreg : ClosureRegime C M n h Ec) : M.gamma ≤ g

The manuscript's parameter block gives every cgamma-threshold.

ClosureRegime n h Ec contains C (cstar M)^{-1} <= Ec and cgamma <= Ec^{-5}. Since cstar M <= 3/2, naming C above (3/2) g^{-1} forces cgamma <= g. Anchor-free.

The large-cube gate, as an eventual statement

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.eventually_recurrenceParams_largeCube {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) : ∀ᶠ (K : ℕ) in Filter.atTop, 10 ^ 10 * M.gamma⁻¹ ≤ ↑↑K - ↑(n + ↑h)

The gate 10^10 cgamma^{-1} <= K - (n+h) of e.recurrence.params holds for every large enough localization cube. Unconditional.

Obligation (1) at the closure families

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.exists_const_eventually_integrable_switchCubeEnergy_closureFamilies (d : ℕ) [NeZero d] (hd : 2 ≤ d) : ∃ (Csplit : ℝ), 0 < Csplit ∧ ∀ (M : ABKModel d) (n : ℤ) (h : ℕ) (Ec : { E : ℝ // 1 ≤ E }) (e e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ClosureRegime Csplit M n h Ec → ∀ᶠ (K : ℕ) in Filter.atTop, ∀ R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) (closureMeshDepth M n h K), MeasureTheory.Integrable (fun (omega : Cutoff.CutoffSample d) => switchCubeEnergy M (n + ↑h) R (principalPz (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e e' R (closureDirichletAlong M n h K e ↑omega) (closureNeumannAlong M n h K e' ↑omega)) omega) ↑(Cutoff.cutoffSampleLaw M)

The first conjunct of SplitScaleObligations, produced inside the manuscript's regime.

For every mesoscopic cell of the closure mesh below a sufficiently large localization cube, the Step-3 switch energy at e.Pz.def's load is sample-integrable under the genuine cutoff law.

exactly on ClosureRegime at the produced threshold and on the two direction bounds.