JunctionDischargeStepFour #

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

The Step-4 gauge junction, discharged at the finite localization cube #

This module discharges Closure.Step4GaugeEndpoint --- the finite-K form of e.lower.bound.pre1, i.e. the manuscript's own inner Jensen display, which is what prescribes in place of the undischargeable limsup form. The passage to the drift is not here: it is the limit passage inside the assembly skeletons of Closure.Junctions.

The chain #

At the Step-4 branch e = 0 and at a unit direction e':

  |Ahom^{1/2} G_{-(h)_R} Ahom^{-1/2} P_R|^2
    = |e' + (grad w_D)_R|^2
      + |(grad w_N + shom^{-1} h e')_R - shom^{-1}(h)_R (e' + (grad w_D)_R)|^2
    = |e'|^2 + |(grad w_N)_R|^2

the second equality being the conjunction of three facts, each supplied below:

cubeAverageVec_eq_zero_of_ae_eq_zero_openCubeSet --- at e = 0 the Dirichlet forcing vanishes identically, so the Dirichlet corrector's gradient is a.e. 0 on cu_K (FreshShellSumZeroDirection) and its average over every descendant cube of cu_K is 0;
cubeAverageVec_streamForcing --- link (i), the cube-average/matVecMul interchange (shom^{-1} h e')_R = shom^{-1} (h)_R e', which is exactly what cancels the shell term of e.Pz.def against the gauge shear of ClosureGaugeCollapse;
blockVecDot_gaugedPrincipalLoadShell_blockDiag_potential --- the resulting per-cube identity, at the terminal's own load.

Averaging over the descendant grid and taking the sample expectation then gives the endpoint through link (ii), descendantsAverage_vecNormSq_cubeAverageVec_le_cubeAverage, the descendant- tiling Jensen step avsum_R |(grad w)_R|^2 <= avg_{cu_K} |grad w|^2: per-cube Jensen, then the exact tiling identity cubeAverage_eq_descendantsAverage_cubeAverage_of_integrableOn.

What is supplied #

integrableOn_cubeSet_of_continuous --- a continuous field is integrable on a triadic cube (a helper for producers discharging the hint binder of link (ii)).
cubeAverageVec_streamForcing --- link (i), unconditional.
descendantsAverage_vecNormSq_cubeAverageVec_le_cubeAverage --- link (ii).
cubeAverageVec_eq_zero_of_ae_eq_zero_openCubeSet --- the descendant-average vanishing of an a.e.-zero field.
blockVecDot_gaugedPrincipalLoadShell_blockDiag_potential --- the per-cube collapse at the Step-4 branch.
step4GaugeEndpoint_of_correctors --- Closure.Step4GaugeEndpoint, proved.

The binders of the endpoint, and their producers #

hD is e.def.w, Dirichlet leg, read at the Step-6 branch direction e = 0; it is the definition of the Dirichlet corrector, not an assumption about it. The remaining four are analytic side conditions of the displays themselves:

binder	content	producer
`hmemN`	`grad w_N^{(K)} in L^2` of each descendant cube	`H1MeanZeroFunction` membership,
restricted along `openCubeSet_subset_of_mem_descendantsAtDepth`
`hintN`	`\|grad w_N^{(K)}\|^2` integrable on `cu_K`	the same membership
`hsampR`	the per-cube energy is sample integrable	`Corrector.CorrectorMeasurableGradient` +
domination by `hsampK`
`hsampK`	`E[\|\|grad w_N^{(K)}\|\|^2_{L2(cu_K)}]` exists
`Corrector.CorrectorLimitNode.integrable_cubeAverage_neumann_energy`

None of them is a mathematical premise of the manuscript's Step 4: each is a measurability/finiteness statement about the very objects the display is about, and each is charged forward to a named proved module. No smallness, no normalization and no bound is assumed.