PerCubeSixWay #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The per-cube six-way Minkowski, and the negation factor two #
What is here #
MinkowskiProviderFinal.lean reduces the anchor to ONE per-cube
L^{p/2}-moment obligation at the L-free Step-3 majorant
Maj(ω) = step3DisplayAt(ω) + step3DisplayAt(Nω) ,
step3DisplayAt = step3FirstTerm + step3SecondTerm + step3ThirdTerm .
This module performs the SIX-WAY Minkowski that splits that obligation into the
three summands, at the sample and at the negated sample, and cancels the second
triple against the first: the negation map preserves the cutoff sample law
(Cutoff.map_negateCutoffSample_cutoffSampleLaw), so
the negated leg has the SAME L^{p/2} moment as the untouched one and the
whole split costs an absolute factor 2.
References #
- ABK26,
l.bounds.mathcal.E.aL,e.apply.sensitivity.J.aL, Step 5.
1. The negation leg has the same moment #
The J3 negation invariance, at the lintegral. Composition with
negateCutoffSample does not change a lower integral against the cutoff sample
law.
2. Two L^q-norm helpers #
3. The six-way split, abstractly #
4. The six-way split at Step 3's display #
The per-cube obligation, split into its three summands.
If the three named summands of Step 3's display obey the development normal
form at exponent q ≥ 1 with majorants R₁, R₂, R₃, then the L-free Step-3
majorant obeys it with majorant 2(R₁+R₂+R₃).
The factor 2 is the negated leg, priced by the proved negation invariance of
the cutoff sample law; no other constant is spent. The three moment inputs and
the three AEMeasurable side conditions are conditional API obligations,
carried as hypotheses rather than instantiated, so that each proved bullet
keeps its own constant.