SubConstFamily #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The triadic coefficient family of a_L − C at a constant skew matrix C #
ABK26, Section 4.1 abbreviates,
ã_{L,m} := a_L − (k_L − k_m)_{□_m}
and then reads the response functional J(z+□_n, …; ã_{L,m}) at every cube
z + □_n of the scale-n lattice. The subtracted matrix is a constant:
the average is taken over the fixed cube □_m, not over the moving cube z + □_n. Consequently ã_{L,m} is a single coefficient field on all of space,
and it carries a genuine Chapter 2 triadic coefficient family — one
coefficient object per cube, all with the same representative.
This is what Support.fluxCorrectedCoeffOn is not: there the average is taken
over the very cube that carries the object, so the field moves with the cube and
no family exists. The two constructions share their ellipticity mechanism, and
this module re-derives it at a free constant.
The ellipticity mechanism #
a_L = ν Id + k_L with k_L antisymmetric, so symmPart a_L = ν Id
(Cutoff.symmPart_coefficientCutoff). Subtracting an antisymmetric constant
C does not move the symmetric part, so symmPart (a_L − C) = ν Id still, and
the lower ellipticity constant is still the molecular diffusivity ν. The
upper constant comes from the entry envelope
Cutoff.coefficientCutoffCubeEntryBound M L ω Q + matAbsSum C, fed to the
public certificate Cutoff.isEllipticMatrix_of_symmPart_and_entry_bound.
Both helpers of the two existing instances of this mechanism
(Cutoff.coefficientCutoffCoeffOn, Support.fluxCorrectedCoeffOn) are
private in their own files, so they are re-derived here rather than reused;
the de-privatisation is a queued cleanup item elsewhere and is deliberately not
performed by this module, which edits no existing file.
What is proved #
subConstCutoffField— the fielda_L − Con all of space, and its symmetric part.subConstCutoffCoeffOn— its Chapter 2 coefficient object on one triadic cube, at the lower constantν.subConstCutoffTriadicCoeffFamily— the triadic family. Compatibility is reflexivity, exactly as forCutoff.coefficientCutoffTriadicCoeffFamily, because every cube receives the same representative.
References #
- ABK26, (
ã_{L,m} := a_L − (k_L − k_m)_{□_m}), (the "differ by a constant anti-symmetric matrix" observation).
The ℓ¹ entry mass of a constant matrix #
The ℓ¹ entry mass of a matrix. It dominates every entry, and is the only
new ingredient the ellipticity of a_L − C needs.
Instances For
The field a_L − C #
The manuscript's ã_{L,m} = a_L − (k_L − k_m)_{□_m}, written at a free
constant C: a single coefficient field on all of space.
Equations
- Algsuperdiff.Section4.Provider.Annular.subConstCutoffField M L C omega x = (Algsuperdiff.Section3.Cutoff.coefficientCutoff M.nu L omega).toFun x - C
Instances For
Subtracting an antisymmetric constant does not move the symmetric part: it
is still exactly ν Id. This is the whole content of the ellipticity of
ã_{L,m}.
The ellipticity constants on one cube #
The uniform entry envelope of a_L − C on Q.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The upper ellipticity constant of a_L − C on Q, produced by the proved
skew-plus-entry-bound certificate.
Equations
Instances For
The coefficient object and the triadic family #
The Chapter 2 coefficient object of ã_{L,m} = a_L − C on the cube Q.
The lower ellipticity constant is still the molecular diffusivity ν, because
the subtracted matrix is antisymmetric.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The triadic coefficient family of ã_{L,m}. Every cube receives the
same literal representative a_L − C; only the locally derived upper
ellipticity witness changes with the cube, so compatibility is reflexivity.
Equations
- One or more equations did not get rendered due to their size.