AntisymmetricShiftCutoff #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The antisymmetric shift at the manuscript's own constant #
AntisymmetricShift.lean proves the invariance for an arbitrary constant skew
matrix. This module instantiates it at the manuscript's own constant
ã_{L,n+2} := a_L − (k_L − k_{n+2})_{z+□_{n+2}} ,
i.e. at Support.fluxCorrectedField, whose subtracted matrix
Support.fluxIncrementAverage is skew because every stream shell is
(a.shell.antisymmetry). The result is the exact display:
-∇·ã_{L,n+2}∇u = -∇·a_L∇u = ∇·g in □_m .
References #
- ABK26,
l.harmonic.approximation.good.scales. - ABK26, (the
ν|∇u|²energy reading).
1. The manuscript's constant is skew #
The averaged flux increment (k_L − k_m)_Q is antisymmetric, in the
matTranspose spelling the shift lemmas consume. Disclosed duplicate: see the
module docstring.
The flux-corrected field is literally the cutoff field minus that constant.
2. The equation at the shifted field #
-∇·ã_{L,k}∇u = ∇·g on any set on which -∇·a_L∇u = ∇·g. No hypothesis
on the set, the solution or the forcing.
The §4.3 Dirichlet problem at the shifted field. The frozen theorem's own
hypothesis IsDirichletSolutionOn a_L □_m u h g yields the same Dirichlet
problem for ã_{L,k}: the boundary clause constrains only u - h.
3. The energy readings of the shifted field #
The symmetric part of ã_{L,k} is exactly ν Id. Public re-derivation
(disclosed duplicate) of the private Support.symmPart_fluxCorrectedField.