GaugeBridge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The Section 4 shell gauges and the Section 3 oscillation gauge #
ABK26 weighs the stream increments in two notations that differ only by where the scale factor sits.
- Section 4 (
d.good.event.for.lambda, andp.mathcalE.annular.decomp) writes the volume-normalized gauge‖∇j‖_{W^{1,∞}(z+□_l)}and multiplies it by3^{(2−γ)l}in the displays. This isSection4.Support.shellW1InfGradNormat the translate: the maximum of‖∇²j‖_{L^∞}and3^{−l}‖∇j‖_{L^∞}. - Section 3 (
e.Bosc.def,e.BoscL.def) writes the same quantity with the factor3^{2l}already distributed inside the maximum, asProvider.BadEvents.cubeOscGauge: the maximum of3^{2l}‖∇²j‖_{L^∞}and3^{l}‖∇j‖_{L^∞}.
The two are literally the same number up to the factor 3^{2l}:
cubeOscGauge Q h = 3^(2 Q.scale) * shellW1InfGradNorm Q.scale
(ShellField.translate (cubeBasePoint Q) h) .
This module records that identity and the three consequences the Section 4 chains need, none of which is stated anywhere else in the repository:
shellW1InfGradNorm_translate_sum_le-- the triangle inequality over a layer sum at the Section 4 gauge, transported fromcubeOscGauge_sum_le. This is the Lean form of the manuscript's repeated step∇(k_b − k_a) = Σ_{l ∈ (a,b]} ∇j_lfollowed by the triangle inequality.shellW1InfGradNorm_translate_shellIncrement_le-- the same at the literal cutoff incrementk_b − k_a.shellW1InfGradNorm_le_zpow_mul_of_le-- the same-centre cube-scale comparisonW(n) ≤ 3^{k−n} W(k)forn ≤ k, which is exactly the manuscript's auxiliary display once the two3^{(2−γ)·}prefactors are restored (see the docstring).
Scope #
The lattice-max enlargement (replacing the maximum over the scale-n lattice
by the maximum over the scale-k lattice) is a covering statement about
latticeCubeSet and is NOT proved here; the comparison below is at a fixed
common centre.
The gauge identity #
The Section 4 / Section 3 gauge identity.
cubeOscGauge is the Section 4 gauge with the factor 3^{2l} pulled inside the
maximum: 3^{2l} max(S, 3^{−l} D) = max(3^{2l} S, 3^{l} D).
The inverse form: the Section 4 gauge is the Section 3 gauge discounted by
3^{−2l}.
The base point of the triadic cube ⟨k, v⟩ is the lattice point
3^k v used by the Section 4 events.
The gauge identity at a lattice centre, in the exact spelling of the Section 4 good events.
The triangle inequality over a layer sum, at the Section 4 gauge #
The layer-sum triangle inequality at the Section 4 gauge.
The Lean form of the manuscript's repeated step: expand ∇(k_b − k_a) as the
finite sum of ∇j_l (tex e.infrared.cutoff.def) and apply the triangle
inequality.
The layer-sum triangle inequality at the literal cutoff increment.
k_b − k_a = Σ_{l ∈ (a,b]} j_l is Cutoff.shellIncrement, so the previous
lemma reads on the genuine increment.
The m-vs-L index bridge, with its tail made explicit.
The clause-(i) chain carries grad (k_L - k_{n-2}) in
e.mathcalE.annular.decomp.pre.zero's third term but grad (k_m - k_{n-2}) in
the Step-3 gradient display; the source performs the substitution silently.
The proved increment calculus does support the bridge, but not as a substitution:
splitting the layer range (a, c] at b produces the head block (a, b] --
the k in [n-1, m] block the Step-3 display resums -- plus a genuine tail
(b, c], which is the k > m block that d.good.event.for.lambda's first
G_1 condition bounds and that becomes pre.zero's fifth term. A caller must
route the tail there; it cannot be absorbed into the head block.
The same-centre cube-scale comparison #
The same-centre cube-scale comparison W(n) ≤ 3^{k−n} W(k) for
n ≤ k, at the origin cube.
This is the content of the manuscript's auxiliary display once its two
prefactors are restored: multiplying both sides by 3^{(2−γ)n} turns it into
3^{(2−γ)n} W(n) ≤ 3^{(1−γ)(n−k)} · 3^{(2−γ)k} W(k) ,
because (1−γ)(n−k) + (2−γ)k − (2−γ)n = k − n.