ClosureGaugeCollapse

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

The per-cube collapse of the gauged doubled quadratic form

ABK26, l.approximate.recurrence.formula, Steps 4 and 5.

Both Step-4 and Step-5 displays start from the same per-cube identity: the gauged doubled quadratic form

| bfAhom_{m-h}^{1/2} G_{-(h)_{z+cu_n}} bfAhom_{m-h}^{-1/2} P_z |^2

collapses to two scalar slots. This module proves that collapse at the exact carrier the closure consumes (gaugedPrincipalLoadShell, the load), once and for all, and reads it at the Step-5 branch e' = 0.

The identity

With

• a = e' + (grad w_D)_R the potential slot,
• b = e + (grad w_N + shom^{-1} h e')_R the flux slot, and
• H = (h)_R = freshShellCubeAverage R omega n m the averaged fresh shell,

the two shom^{±1/2} normalizations of P_z cancel against the two diagonal weights shom^{±1} and the identity is

|a|^2 + |b - shom^{-1} H a|^2.

That is exactly the right-hand side of the manuscript's own per-cube displays: there at e = 0, w_D = 0, and there at e' = 0, w_N = 0, expanded into its four terms.

What is supplied

• blockVecDot_gaugedPrincipalLoadShell_blockDiag — the collapse, at every direction pair. It is an unconditional algebraic identity: no solution, measurability, selection or normalization property of wD, wN is used, and no binder is carried.
• neumannFluxField_zero_direction — at e' = 0 the flux leg field is the bare Neumann corrector gradient, the fresh-shell term of e.Pz.def vanishing with its direction.
• blockVecDot_gaugedPrincipalLoadShell_blockDiag_flux — the collapse read at the Step-5 branch e' = 0, again unconditionally. The remaining (grad w_N)_R is killed by Provider.Diffusivity.Corrector.FreshShellSumZeroDirection at any consumer that carries the Neumann weak-solution binder; that reduction is deliberately not performed here, so that this module stays hypothesis-free.

What is not here

Neither Step-4 nor Step-5 endpoint is proved, and neither Closure.Step4GaugeEndpoint nor Closure.Step5GaugeEndpoint is discharged: those need the corrector-energy display at the localization grid, which is a different obligation. Nothing below realizes a source node.

References

• ABK26, e.Pz.def; the gauged load.
• ABK26, e.lower.bound.pre1; e.lower.bound.pre2.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_gaugedPrincipalLoadShell_blockDiag {d : ℕ} (sigma : Observable.PositiveScalar) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (n m : ℤ) (e e' : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (omega : Cutoff.ShellSeq d) : HCPolySupport.blockVecDot (gaugedPrincipalLoadShell sigma R n m e e' wD wN omega) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockDiag (↑sigma • 1) ((↑sigma)⁻¹ • 1)) (gaugedPrincipalLoadShell sigma R n m e e' wD wN omega)) = HCPolySupport.vecNormSq (e' + HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => (wD omega).grad x) + HCPolySupport.vecNormSq (e + HCPolySupport.cubeAverageVec R (neumannFluxField sigma omega n m e' (wN omega)) - (↑sigma)⁻¹ • HCPolySupport.matVecMul (freshShellCubeAverage R omega n m) (e' + HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => (wD omega).grad x))

The per-cube collapse of the gauged doubled quadratic form.

The two shom^{±1/2} normalizations of P_z cancel against the two diagonal weights shom^{±1}, leaving the potential slot |e' + (grad w_D)_R|^2 and the sheared flux slot |(e + (grad w_N + shom^{-1} h e')_R) - shom^{-1} (h)_R (e' + (grad w_D)_R)|^2.

Unconditional: wD and wN are bare families and nothing is assumed of them.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.neumannFluxField_zero_direction {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (n m : ℤ) {Q : HCPolySupport.TriadicCube d} (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : neumannFluxField sigma omega n m 0 wN = fun (x : HCPolySupport.Vec d) => wN.toH1Function.grad x

At the zero flux direction the flux leg field of e.Pz.def is the bare Neumann corrector gradient: the fresh-shell term shom^{-1} h e' vanishes with its direction.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_gaugedPrincipalLoadShell_blockDiag_flux {d : ℕ} (sigma : Observable.PositiveScalar) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (n m : ℤ) (e : HCPolySupport.Vec d) (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) (omega : Cutoff.ShellSeq d) : HCPolySupport.blockVecDot (gaugedPrincipalLoadShell sigma R n m e 0 wD wN omega) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockDiag (↑sigma • 1) ((↑sigma)⁻¹ • 1)) (gaugedPrincipalLoadShell sigma R n m e 0 wD wN omega)) = HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => (wD omega).grad x) + HCPolySupport.vecNormSq ((e + HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => (wN omega).toH1Function.grad x) - (↑sigma)⁻¹ • HCPolySupport.matVecMul (freshShellCubeAverage R omega n m) (HCPolySupport.cubeAverageVec R fun (x : HCPolySupport.Vec d) => (wD omega).grad x))

The collapse at the Step-5 branch e' = 0.

Still unconditional. A consumer carrying the Neumann weak-solution binder of e.def.w kills the remaining (grad w_N)_R by FreshShellSumZeroDirection.grad_ae_eq_zero_of_isMeanZeroNeumannRhsWeakSolution_streamForcing_zero, leaving the manuscript's |(grad w_D)_R|^2 + |e - shom^{-1} (h)_R (grad w_D)_R|^2.