UglyLatticeChain #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
e.ugly.estimate.for.J read at a lattice cube z + cu_n #
ABK26, Section 4.1. Step 2 of p.mathcalE.annular.decomp states the ugly
estimate "on each cube z + cu_n", while the Section 2.4 sensitivity anchor it
cites lives on the unit cube cu_0. Four slot transports close the gap, and
this module runs all four at once:
- the gradient leg --
GradNormalization.gradientW1Infinity_centeredShellUnitCube_le; - the value leg --
ValueBridge.valueL2_sq_centeredShellUnitCube_le.
The output is Ugly.IsUglyJEstimate with every slot at a manuscript object
on the lattice cube ⟨n, v⟩ = 3^n v + cu_n: the response of tilde a_{L,m},
the annular (2,2) error atom at the translated sample, the sigma-bar ratio,
the L^infinity content of k_m - k_{n-2} on z + cu_n, the
W^{1,infinity} gauge of grad (k_L - k_{n-2}) on z + cu_n and the same
gauge of grad (k_L - k_m) on cu_m.
The s <= 1/4 residual, carried honestly #
The anchor needs both of its exponent slots in (0, 1/4]; the enclosing
proposition admits s in [8 gamma, 1/2]. hs14 below is that restriction,
stated and never hidden.
The conservative L^infinity reading #
The third slot is produced at the L^infinity norm of k_m - k_{n-2} on
z + cu_n where the manuscript prints the volume-normalized L^2 norm of the
same increment on the same cube. This is the dominating direction and it is
exactly the reading A2b's annularL2Block consumes; see ValueBridge.lean for
the carrier discussion.
Part A -- splitting the gradient gauge at an intermediate scale #
The gradient gauge splits at an intermediate scale.
|| grad (k_c - k_a) ||_{W^{1,infinity}(z+cu_k)} is at most the sum of the
two partial gauges. This is the Lean form of the manuscript's m-versus-L
bookkeeping: the head block (a, b] feeds
e.mathcalE.annular.decomp.pre.zero's fourth term and the tail block (b, c]
its fifth.
The cross-scale comparison of the gradient gauge, at a lattice centre.
For a scale-n lattice point z of cu_m the annulus cube z + cu_n sits
inside cu_m, so the volume-normalized W^{1,infinity} gauge on z + cu_n
is at most 3^{m-n} times the one on cu_m. This is the manuscript's
auxiliary step (|| grad j_k ||_{W^{1,infinity}(z+cu_n)} replaced by 3^{m-n} || grad j_k ||_{W^{1,infinity}(cu_m)}), which
Support.shellW1InfGradNorm_le_zpow_mul_of_le supplies only at a common
centre.
The gradM-slot monotonicity of the five-term display, at the fifth
slot's weight C c_*^{-1} gamma w_gamma.
Part B -- the composed per-cube estimate at a lattice cube #
e.ugly.estimate.for.J at the lattice cube ⟨n, v⟩.
The Section 2.4 sensitivity anchor, collapsed by UglyChain and read through
the four slot transports, at the manuscript's own perturbation `h = k_L - (k_L
- k_m){cu_m} - k{n-2}
and its own coefficienttilde a_{L,m} = a_L - (k_L - k_m)_{cu_m}`.
Every quantity on both sides is a manuscript object on 3^n v + cu_n; nothing
unit-cube remains.