TranslationTransportAssembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The equation leg of the interior clause, assembled #
Starting from the frozen theorem's own datum
IsDirichletSolutionOn a_L(·,ω) □_m u h g
and its own interior gate (z+□_{n+2}) ∩ ∂□_m = ∅, it produces
IsForcedEquation □_{n+2}
(fluxCorrectedCoeffFamily M L (n+2) □_{n+2} (translateCutoffSample z ω))
(u(· + z)) (fun x => -g(x + z))
The three steps:
- restriction to
z + □_{n+2}—EquationRestriction.lean, driven by the anchor's frontier-empty gate; - untranslation to
□_{n+2}attranslateCutoffSample z ω—TranslationTransport.lean; - the antisymmetric shift
a_L ↦ ã_{L,n+2}—AntisymmetricShift{,Cutoff}.lean.
Step 3 is performed after the untranslation, so the subtracted constant is
(k_L − k_{n+2})_{□_{n+2}} computed at the translated sample — which, by the
exact translation identity of step 2, is the manuscript's (k_L − k_{n+2})_{z+□_{n+2}}. The order is immaterial (the constant is
translation-inert), but this order is the one in which every proved cap is
stated.
What the forcing becomes, exactly #
The translated frame's forcing is x ↦ -g(x + z); the sign is CoarseGraining's
∇·g convention (Support/Dirichlet.lean) and the translation is the A4 frame
move. Both are invisible to the frozen theorem's right-hand side, whose
g-legs are seminorms ([g]_{H^s}), even and translation-covariant.
References #
- ABK26,
l.harmonic.approximation.good.scales.
1. The coefficient field of the flux-corrected family #
The representative of Support.fluxCorrectedCoeffFamily on every cube is the
literal flux-corrected field.
2. The assembled equation leg #
The interior clause's equation hypothesis, produced from the anchor's own datum.
Restriction to the parent window, the A4 untranslation, and the antisymmetric shift, composed.
The same, entered at the frozen theorem's IsDirichletSolutionOn datum.
3. The transported solution, read pointwise #
The transported solution's value: it is u(· + z), with no modification.