LocalizationOscillationEndpointSixteen

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

e.lower.bound.oscillations at the interior mesh, one power of gamma sharper

LocalizationOscillationEndpoint proves the interior-mesh endpoint of e.lower.bound.oscillations at gamma^{15}, the manuscript's own exponent. The transport of that endpoint from the interior meso grid to the full mesh costs a boundary remainder, so the interior half has to be delivered with one power of gamma to spare if the sum is to stay below gamma^{15}.

This module supplies that sharper interior endpoint. Nothing in the proved gamma^{15} route is edited: the sharpening is a re-instantiation of the same three inputs

• LocalizationOscillationDisplay.exists_freshShell*_gradient_oscillation_lower_bound_display,
• LocalizationEnvelopeWire.exists_freshShell_gridFourthMoment_mesoWindowEnergy_le_wired,

exists_gamma0_integrable_freshShell*_meshEnergyCell_rpow_four,

at the same explicit threshold min gcell (min (1/4) (min genv (min 3^{-(d+3)} (1/(1+Ctot))))).

Where the spare power comes from

LocalizationOscillationBudget.three_term_budget_le collapses the display's three terms to Ctot gamma^{31} and then uses hfinal : Ctot gamma^{16} <= 1 to land on gamma^{15}. But the threshold that produces hfinal is gamma <= 1/(1 + Ctot), which gives Ctot gamma <= 1 outright; since gamma <= 1, it gives Ctot gamma^k <= 1 for every k >= 1, in particular for k = 15. That is the slack the module docstring of the proved endpoint does not use: the 1/(1+Ctot) factor in its min is one power stronger than the gamma^{15} conclusion needs.

three_term_budget_le_mul below is the proved collapse stopped one step earlier, at Ctot gamma^{31}; three_term_budget_le_sixteen is the k = 15 instance of the last step. The proved three_term_budget_le is the k = 16 instance and is untouched.

What is proved

• three_term_budget_le_mul -- the three-term collapse, at Ctot gamma^{31}.
• three_term_budget_le_sixteen -- its gamma^{16} form.
• exists_gamma0_freshShellDirichlet_meshOscillation_le_gamma_pow_sixteen and its Neumann mirror -- the interior endpoint at gamma^{16}. Statement, binders and threshold are those of the proved ..._fifteen pair, with 15 replaced by 16 in the conclusion and nothing else changed.

Binders

Verbatim those of LocalizationOscillationEndpoint: hd, the model gate M.gamma <= gamma0, the induction state, the four source gates 0 < h, m - h <= m0, h <= 6 cstar gamma^{-1}, 10^10 gamma^{-1} <= K - m, the two direction bounds, the base point z0, and the corrector family with the weak formulation of e.def.w. No sample-space binder survives, for the same reason as there.

Scope

There is no sorry.

References

• ABK26, e.lower.bound.oscillations, e.recurrence.params, e.def.w.

The three-term collapse, stopped one step earlier

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.three_term_budget_le_mul {C W Csig sqd Nr G P S Eb gamma Ctot Kn : ℝ} (hC : 0 ≤ C) (hW : 0 ≤ W) (hCsig : 0 ≤ Csig) (hsqd : 0 ≤ sqd) (hNr0 : 0 ≤ Nr) (hG0 : 0 ≤ G) (_hP0 : 0 ≤ P) (_hS0 : 0 ≤ S) (hEb0 : 0 ≤ Eb) (_hKn0 : 0 ≤ Kn) (hgamma0 : 0 < gamma) (hgamma1 : gamma ≤ 1) (hG : G ≤ gamma ^ 32) (hSP : S * P ≤ Csig) (hNr : Nr * gamma ≤ Kn) (hEb : Eb ≤ 1) (hCtot : C * W + Kn * (C * sqd * Csig) + C * Csig ≤ Ctot) : C * (G * W) + C * (Nr * (S * sqd * Eb)) * (G * P) + C * S * (G * P) ≤ Ctot * gamma ^ 31

The three surviving terms of e.lower.bound.oscillations, at Ctot gamma^{31}. This is LocalizationOscillationBudget.three_term_budget_le with its last step -- the absorption of Ctot into a power of gamma -- removed, so that the caller may choose which power to land on.

: purely on the displayed numeric hypotheses; no model, field or measure occurs.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.three_term_budget_le_sixteen {C W Csig sqd Nr G P S Eb gamma Ctot Kn : ℝ} (hC : 0 ≤ C) (hW : 0 ≤ W) (hCsig : 0 ≤ Csig) (hsqd : 0 ≤ sqd) (hNr0 : 0 ≤ Nr) (hG0 : 0 ≤ G) (hP0 : 0 ≤ P) (hS0 : 0 ≤ S) (hEb0 : 0 ≤ Eb) (hKn0 : 0 ≤ Kn) (hgamma0 : 0 < gamma) (hgamma1 : gamma ≤ 1) (hG : G ≤ gamma ^ 32) (hSP : S * P ≤ Csig) (hNr : Nr * gamma ≤ Kn) (hEb : Eb ≤ 1) (hCtot : C * W + Kn * (C * sqd * Csig) + C * Csig ≤ Ctot) (hfinal : Ctot * gamma ^ 15 ≤ 1) : C * (G * W) + C * (Nr * (S * sqd * Eb)) * (G * P) + C * S * (G * P) ≤ gamma ^ 16

The gamma^{16} form of the three-term collapse. Identical to LocalizationOscillationBudget.three_term_budget_le except that the absorption gate is Ctot gamma^{15} <= 1 and the conclusion is gamma^{16}.

The two sharpened endpoints

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_gamma0_freshShellDirichlet_meshOscillation_le_gamma_pow_sixteen (d : ℕ) (hd : 2 ≤ d) : ∃ (gamma0 : ℝ), 0 < gamma0 ∧ gamma0 ≤ 1 / 4 ∧ ∀ (M : ABKModel d), M.gamma ≤ gamma0 → ∀ (m0 : ℤ) (Eind : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Eind → ∀ (m K : ℤ) (h : ℕ), 0 < h → m - ↑h ≤ m0 → ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → 10 ^ 10 * M.gamma⁻¹ ≤ ↑K - ↑m → ∀ (e e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ∀ (z₀ : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d K))), (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M (m - ↑h)))⁻¹ omega (m - ↑h) m e x) → (gridFourthMomentRoot (↑M.P) (interiorMesoCubeGrid d K (recurrenceMesoScale recurrenceGapMultiplier M.gamma m ↑h) (m - ↑h - 1)) fun (R : HCPolySupport.TriadicCube d) (omega : ℤ → Frozen.Assumptions.ShellField d) => meshOscillationCell (recurrenceMesoScale recurrenceGapMultiplier M.gamma m ↑h) (wD omega).grad R) + (↑(Annealed.sigmaBar M (m - ↑h)))⁻¹ * (3 ^ ↑(recurrenceMesoScale recurrenceGapMultiplier M.gamma m ↑h) * (∫ (omega : Cutoff.ShellSeq d), shellDerivNormSum (m - ↑h) m z₀ omega ^ 4 ∂↑M.P) ^ 4⁻¹) ≤ M.gamma ^ 16

e.lower.bound.oscillations for the Dirichlet corrector of e.def.w, at the recurrence parameters, below gamma^{16}.

Statement, binders and threshold are those of exists_gamma0_freshShellDirichlet_meshOscillation_le_gamma_pow_fifteen; only the conclusion's exponent changes.