GradNormalization #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The gradient-slot cube-scale normalization of e.ugly.estimate.for.J.pre #
ABK26, Section 4.1.
3^{2n} || grad (k_L - k_{n-2}) ||_{W^{1,infinity}(z + cu_n)}
, whereas the cited lemma carries the unit-cube gauge || grad h ||_{W^{1,infinity}(cu_0)}/4182. The replacement is made with no comment; it is
the gradient half of the same silent rescaling whose error half is
ErrorTransport.lean and whose response half is ResponseTransport.lean.
This module proves that half.
What was already there, and what is added #
ApproximateRecurrence.centeredShellUnitCube_gradientW1Infinityisrflonto(incrementUnitCube₂ ⟨n,v⟩ lowScale L omega).gradientW1Infinity: the manuscript's centering constant(k_L - k_m)_{cu_m}is invisible to the gradient slot, for free.BadEvents.gradientW1Infinity_incrementUnitCube₂_lebounds that byincrementOscGauge₂, i.e. bycubeOscGaugeof the literal increment.Support.cubeOscGauge_mk_eq_zpow_mul_shellW1InfGradNormis the identitycubeOscGauge ⟨n,v⟩ h = 3^{2n} · shellW1InfGradNorm n (translate (3^n v) h).
What is added here is (i) the composition of the three at the Section 4 lattice
enumerations, in the Real.rpow spelling the ugly chain reads, and (ii) the
slot monotonicity of IsUglyJEstimate, which is what lets the chain be fed an
inequality where UglyChain.exists_responseJ_ugly_estimate demands an
equality. Without (ii) the normalization is unusable: the gauge comparison is
one-sided in the direction of the estimate, never an identity.
The re-gauged chain #
exists_responseJ_ugly_estimate_of_grad_le is
UglyChain.exists_responseJ_ugly_estimate with the binder
h.gradientW1Infinity = 3^{2n} Gn weakened to h.gradientW1Infinity ≤ 3^{2n} Gn
and with the same conclusion. The proof runs the original chain at the exact
witness Gn' := 3^{-2n} · h.gradientW1Infinity and then enlarges the fourth
slot. The nonnegativity of the output constant C is derived, not assumed:
Cl ≥ 0 follows from the good-event budget hlam and Cr ≥ 0 from the
sigmaBar ratio, and the remaining factors are squares.
The s ≤ 1/4 residual #
Unchanged and carried honestly: the Section 2.4 sensitivity anchor needs both
exponent slots in (0, 1/4] while the enclosing proposition admits s ∈ [8γ, 1/2]. Nothing here narrows or hides that; see UglyPre.lean.
The zpow/rpow bridge at the cube-scale factor #
The normalization itself #
The frozen unit-cube gradient gate of the manuscript's own perturbation
h = k_L - (k_L - k_m)_{cu_m} - k_{n-2}, rescaled onto the unit cube at the
lattice cube ⟨n, v⟩ = 3^n v + cu_n, is bounded by the manuscript's printed
slot
3^{2n} || grad (k_L - k_{lowScale}) ||_{W^{1,infinity}(3^n v + cu_n)} .
The centering constant has already disappeared (it is invisible to a gradient gauge), so this is exactly the cube-scale normalization and nothing else.
The same at the 𝒢₂ cutoff level n − 2, i.e. in the exact spelling in
which e.ugly.estimate.for.J.pre reads the slot.
Slot monotonicity of IsUglyJEstimate #
The gradN-slot monotonicity of the five-term display. Enlarging the
fourth slot preserves the estimate; the three sign conditions are the ones the
weight C c_*^{-1} γ w needs.
The L2-slot monotonicity of the five-term display. Its twin at the
third slot; the conservative L^infinity-for-L^2 reading of the clause-(i)
third term is consumed through this lemma.
The-slot monotonicity of the five-term display, at the first slot's weight
C w.
The re-gauged chain #
The composed per-cube estimate, at an inequality in the gradient slot.
UglyChain.exists_responseJ_ugly_estimate demands
h.gradientW1Infinity = 3^{2n} Gn. The cube-scale normalization above is a
one-sided comparison -- the gauge of the rescaled increment is bounded by the
manuscript's slot, never equal to it -- so the chain has to be read at an
inequality. This is that reading, with the same conclusion and the same
constants.