Junctions

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

The two junctions of the closure node, and the assembly skeletons

The two-sided closure of l.approximate.recurrence.formula needs three things beyond the arithmetic of Closure.StepSixClosure:

1. the principal comparison, proved: exists_const_descendantsAverage_integral_principalEnergy_le_annealedLimit;
2. the gauge endpoints of Steps 4 and 5 (e.lower.bound.pre1, and e.lower.bound.pre2), whose fresh-shell energy display is produced by the lane shellsum-limit (Corrector territory);
3. the basic split with its localization remainder (e.lower.bound.basic.split, and e.lower.bound.localization.terms) together with the passage P . bfAhom_m P = lim_K E[P . bfA_m(cu_K) P], whose cgamma^10 endpoint is produced by the lane gamma10-final.

Items 2 and 3 are in flight. This module therefore does two things:

• it proves the assembly skeletons: given those propositions, the printed displays follow. When the producers land, each premise is discharged by a single exact.

The proved terminal itself is deliberately not imported: this module uses only the carriers it is stated about (switchCubeEnergy, principalPz, gaugedPrincipalLoadShell, principalResponseSwitchBudget), so importing the terminal would add elaboration weight without adding content. The consumer that discharges PrincipalSwitchEndpoint imports both.

These are the only caller-supplied mathematical propositions in this lane. They are marked private where they are assembly skeletons; the named endpoint Props themselves are public only so that a producer can state that it proves one. Nothing here realizes a source node, and nothing here is a public node claim.

The gauge junctions carry the FINITE-K corrector energies

An earlier revision of this module stated the two gauge junctions with the manuscript's limit drift constant shom_n^{-2} cstar (log 3) sum_{k in Ioc n (n+h)} 3^{2 cgamma k} at a single fixed localization cube cu_K. That form is undischargeable, and this is the failure recorded: after the gauge collapse (ApproximateRecurrence.ClosureGaugeCollapse), Step 4's right-hand side is 1 + E || grad w_N^{(K)} ||^2_{L2(cu_K)} whose energy decreases to the drift, so at finite K it is >= the drift and never <= it; Step 5's is 1 - E || grad w_D^{(K)} ||^2_{L2(cu_K)} + ... whose energy increases to the drift, so at finite K it is <= the drift and again on the wrong side. The manuscript itself only ever asserts the two displays under a limsup_K, and its own inner step is the finite-K Jensen inequality.

That prescription is carried out here:

• Step4GaugeEndpoint and Step5GaugeEndpoint are restated at the finite-K corrector energies neumannCubeEnergy and dirichletCubeEnergy, i.e. at exactly the manuscript's inner display;
• the drift comparison moves into the assembly skeletons as a limit passage: the two shom-ratio displays RecurrenceUpperDisplay, RecurrenceLowerDisplay are K-independent, so the skeletons consume the whole family of finite-K junctions together with the convergence of the corrector energy to the drift, and pass K -> infinity with vanishing slack.

The convergence input is proved, as Provider.Corrector.ShellSumEnergyDisplay.tendsto_integral_cutoffSample_cubeAverage_display at gauge c = shom_n^{-1} and unit direction: its limit is shellDrift M n h by shellDrift_eq_shellSum, its Neumann half is the Step-4 input and its Dirichlet half the Step-5 input. The sharp sandwich halves behind it are Provider.Corrector.NeumannUpperBound and Provider.Corrector.DirichletLowerBound.

The corrector families are indexed by the increment path

The proved terminal's load gaugedPrincipalLoadShell indexes the corrector families by the shell sequence ShellSeq d, while e.def.w and the energy display index them by the increment path C(Vec d, Mat d) --- which is the honest reading, the forcing depending on the sample only through k_{n+h} - k_n. The junctions below take the producers' indexing and compose with Provider.Corrector.shellSumValuePath; the composition is named alongIncrementPath so that the bridge is explicit at every use.

The carriers

Instantiating the terminal at m := n + h, hgap := h therefore leaves one integer rewrite, n + h - h = n, before the exact; that rewrite is the only difference between the terminal's conclusion and PrincipalSwitchEndpoint.

Constants

closureConstant is the absolute constant that folds the switch cross term `(1

• shellIncrementCap) * deltaand the two additive remainderscgamma^6, cgamma^10under the printed budgetC E^2 |log cgamma|^2 cgamma`.

References

• ABK26, l.approximate.recurrence.formula, Steps 4--6.

The two carriers of the terminal, re-indexed by (n, h)

@[reducible, inline]

noncomputable abbrev Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.principalEnergyAverage {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (j : ℕ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) : ℝ

The left-hand side of the proved principal-response terminal, at the recurrence pair (n, n+h): the depth-j descendant average of the annealed localized principal energy.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gaugeEnergyAverage {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (j : ℕ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) : ℝ

The right-hand side of the proved principal-response terminal, at the recurrence pair (n, n+h): the depth-j descendant average of the annealed gauged load quadratic against bfAhom_n. This is the left-hand side of both e.lower.bound.pre1 and e.lower.bound.pre2.

Equations

• One or more equations did not get rendered due to their size.

The shell sum, in the two index conventions

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.sum_Ioc_eq_sum_Icc (gamma : ℝ) (n : ℤ) (h : ℕ) : ∑ k ∈ Finset.Ioc n (n + ↑h), 3 ^ (2 * gamma * ↑k) = ∑ k ∈ Finset.Icc (n + 1) (n + ↑h), 3 ^ (2 * gamma * ↑k)

The manuscript writes the shell sum as sum_{k = m-h+1}^m; the in-flight fresh-shell display carries it as a sum over Finset.Ioc (m-h) m. At the recurrence pair the two are the same finite set.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.shellDrift_eq_shellSum {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) : shellDrift M n h = (↑(Annealed.sigmaBar M n) ^ 2)⁻¹ * (Disorder.cstar M * Real.log 3 * ∑ k ∈ Finset.Ioc n (n + ↑h), 3 ^ (2 * M.gamma * ↑k))

The fresh-shell display's right-hand constant is shellDrift.

The indexing bridge and the finite-K corrector energies

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.alongIncrementPath {d : ℕ} {alpha : Type u_1} (n : ℤ) (h : ℕ) (w : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → alpha) : Cutoff.ShellSeq d → alpha

The indexing bridge.

The producers of the gauge junctions (e.def.w and the fresh-shell energy display) deliver the corrector families indexed by the increment path `k_{n+h}

• k_n; the proved terminal's load gaugedPrincipalLoadShell` indexes them by the shell sequence. This is the composition, written once so that the bridge is visible at every use.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.alongIncrementPath n h w omega = w (Algsuperdiff.Section3.Provider.Corrector.shellSumValuePath n (n + ↑h) omega)

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.neumannCubeEnergy {d : ℕ} (M : ABKModel d) (n : ℤ) (h K : ℕ) (wN : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))) : ℝ

The finite-K Neumann corrector energy E[ || grad w_N^{(K)} ||^2_{L2(cu_K)} ], at the recurrence consumer's carrier.

This is, verbatim, the left-hand side of the Neumann half of Provider.Corrector.ShellSumEnergyDisplay.tendsto_integral_cutoffSample_cubeAverage_display, whose limit as K -> infinity is the drift shellDrift M n h at gauge c = shom_n^{-1} and unit direction.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.dirichletCubeEnergy {d : ℕ} (M : ABKModel d) (n : ℤ) (h K : ℕ) (wD : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))) : ℝ

The finite-K Dirichlet corrector energy E[ || grad w_D^{(K)} ||^2_{L2(cu_K)} ], at the recurrence consumer's carrier.

This is the left-hand side of the Dirichlet half of the same proved display, and its limit is again shellDrift M n h.

Equations

• One or more equations did not get rendered due to their size.

The named junction premises

Each definition below is a proposition supplied by a named producer. None is proved here; each is consumed as a binder by the assembly skeletons at the end of this module.

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.Step4GaugeEndpoint {d : ℕ} (M : ABKModel d) (n : ℤ) (h K j : ℕ) (e' : HCPolySupport.Vec d) (wD : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))) (wN : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))) : Prop

The manuscript's Step-4 display is asserted under a limsup_K; its right-hand side is the limit constant shom_n^{-2} cstar (log 3) sum_{k in Ioc n (n+h)} 3^{2 cgamma k}. Per that form cannot be a junction premise --- the consumer is an inequality between two numbers at one grid, and the finite-K Neumann energy lies on the wrong side of the limit. What the manuscript actually proves before passing to the limit is the inner Jensen display

  avsum_z | Ahom^{1/2} G_{-(h)_z} Ahom^{-1/2} P_z |^2
    = |e'|^2 + avsum_z |(grad w_N^{(K)})_z|^2
    <= |e'|^2 + || grad w_N^{(K)} ||^2_{L2(cu_K)} ,

and that is what is stated here, at |e'| = 1, in expectation, and at the terminal's carrier. The passage to the drift is done by the assembly skeletons below, from the proved convergence.

: Closure.JunctionDischargeStepFour, composing

• the gauge collapse ApproximateRecurrence.ClosureGaugeCollapse.blockVecDot_gaugedPrincipalLoadShell_blockDiag;
• the zero-direction vanishing grad_ae_eq_zero_of_isZeroTraceDirichletRhsWeakSolution_streamForcing_zero (the e = 0 branch of Step 6, where the Dirichlet corrector's forcing vanishes identically, so w_D = 0 and (grad w_D)_R = 0);
• the cube-average/matVecMul interchange cubeAverageVec R (streamForcing c omega n m e') = c . (h)_R e', which is what cancels the shell term of e.Pz.def against the gauge shear;
• the descendant-tiling Jensen step avsum_R |(grad w)_R|^2 <= avg_{cu_K} |grad w|^2.

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.Step5GaugeEndpoint {d : ℕ} (M : ABKModel d) (n : ℤ) (h K j : ℕ) (e : HCPolySupport.Vec d) (Fend : ℝ) (wD : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))) (wN : C(HCPolySupport.Vec d, HCPolySupport.Mat d) → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))) : Prop

Mirroring Junction 1: the manuscript's limsup_K display is replaced by the finite-K inequality it is deduced from. The manuscript's own chain is

  avsum_z E| ... |^2
    = |e|^2 + avsum_z E[ |(grad w_D^{(K)})_z|^2
        + shom^{-2}|(h)_z (grad w_D^{(K)})_z|^2
        - 2 shom^{-1} e . (h)_z (grad w_D^{(K)})_z ]
    <= |e|^2 + shom^{-2} E|| h grad w_D^{(K)} ||^2_{L2(cu_K)}
        - E|| grad w_D^{(K)} ||^2_{L2(cu_K)} + cgamma^15 ,

whose first positive term is bounded by Fend h^2 shom_n^{-4} 3^{4 cgamma(n+h)} via Closure.shellProduct_le_quadratic_error, and whose negative term is the finite-K Dirichlet energy of dirichletCubeEnergy. The drift only appears after K -> infinity, which the skeletons below perform.

: Closure.JunctionDischargeStepFive, composing the gauge collapse read at e' = 0 (ClosureGaugeCollapse.blockVecDot_gaugedPrincipalLoadShell_blockDiag_flux), the zero-direction vanishing of the Neumann leg (grad_ae_eq_zero_of_isMeanZeroNeumannRhsWeakSolution_streamForcing_zero), the Hoelder product Closure.shellProduct_le_quadratic_error (on l.km.kn.Lp and e.nablaw.in.L.eight), and the proved cgamma^15 oscillation endpoint (exists_gamma0_freshShellDirichlet_meshOscillation_le_gamma_pow_fifteen).

Fend is the endpoint's own constant for the quadratic h-error; it is left free here and enters the printed display only through max. The directional factor |e|^2 restored is 1, this being the |e| = 1 branch. The Neumann direction is 0: the e' = 0 branch of Step 6, where the Neumann forcing vanishes, so w_N = 0 and the flux slot of gaugedPrincipalLoadShell collapses to the manuscript's bare e, the shell term shom_n^{-1} h e' being 0 as well.

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.AnnealedSplitEndpoint {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (j : ℕ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) : Prop

Junction 3 --- the basic split, its localization remainder, and the annealed limit passage.

, jointly:

• the proved structural split LocalizationRecurrenceMesh.exists_localizationRecurrenceMeshSplit_le_descendantsAverage_expanded;
• lane gamma10-final --- the cgamma^10 fluctuation endpoint (e.lower.bound.localization.terms) at the same descendantsAverage carrier;
• the annealed identification P . bfAhom_m P = lim_K E[P . bfA_m(cu_K) P], available from Annealed.sigmaBar_characterization, which is the root assembly's step rather than an endpoint.

The premise is stated as a single inequality because that is how the three enter Step 6: the doubled form at the annealed limit is dominated by the localized principal average plus the cgamma^10 localization remainder.

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.PrincipalSwitchEndpoint {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (j : ℕ) (Ec : { E : ℝ // 1 ≤ E }) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) : Prop

Junction 4 --- the proved principal comparison, at this indexing.

: already proved, as exists_const_descendantsAverage_integral_principalEnergy_le_annealedLimit; this is only its re-indexing from (m - h, m) to (n, n + h), at the witness pair wD, wN that the terminal itself produces.

This Prop itself does not reach it, and a discharge of it from the terminal inherits the reach but no incomplete-proof axiom. See the module header's Disclosure section.

Equations

• One or more equations did not get rendered due to their size.

The absorbing constant

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureConstant : ℝ

The absolute constant of the closure: it folds the switch cross term and the three additive remainders cgamma^6, cgamma^10, cgamma^15 under the printed budget. It depends on nothing --- not on the dimension, the model, the scales or the parameters.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.principalResponseSwitchBudget_eq {d : ℕ} (M : ABKModel d) (Ec : { E : ℝ // 1 ≤ E }) : principalResponseSwitchBudget M Ec 64 = principalResponseBudgetConst * 3 ^ 128 * (↑Ec ^ 2 * Real.log M.gamma ^ 2 * M.gamma)

The printed switch budget, unfolded.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gamma_le_one_of_le_exp_neg_one {gamma : ℝ} (hgamma : gamma ≤ Real.exp (-1)) : gamma ≤ 1

The absorption.

On the manuscript's own smallness cgamma <= exp (-1) (which e.cgamma.constraints implies, E >= 1 giving cgamma <= E^{-5} <= 1 and the enlarged M giving the rest), the switch cross term together with the cgamma^6 and cgamma^10 remainders is below the printed budget at the absolute constant closureConstant.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.switch_and_remainders_le_flatError {d : ℕ} (M : ABKModel d) (Ec : { E : ℝ // 1 ≤ E }) (hgamma : M.gamma ≤ Real.exp (-1)) : (1 + shellIncrementCap) * (3 * principalResponseSwitchBudget M Ec 64) + (M.gamma ^ 6 + M.gamma ^ 10) + 2 * M.gamma ^ 15 ≤ recurrenceFlatError M closureConstant ↑Ec