UglyChain

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The e.ugly.estimate.for.J.pre to e.ugly.estimate.for.J composition

ABK26, Section 4.1. This module closes the chain: UglyPre produces the four sensitivity terms from the Section 2.4 anchor, and Ugly collapses them against the good-event budgets. The composition below runs both, so the only remaining inputs are the manuscript's own displayed facts.

Here it is discharged.

The two silent normalizations, made explicit

• hgrad --- the caller supplies Gn with h.gradientW1Infinity = 3^{2n} Gn. This is exactly the manuscript's unremarked replacement of the unit-cube gauge ||grad h||_{W^{1,infinity}(cube_0)} by the scale-normalized 3^{2n} ||grad(k_L - k_{n-2})||_{W-underline^{1,infinity}(z+cube_n)}.
• The cube itself. Every carrier here is the unit cube of the anchor; the manuscript's translation and rescaling to z + cube_n is not performed.

The s <= 1/4 residual

hs14 is the honest range: the cited sensitivity lemma requires its exponent slots in (0, 1/4], and the manuscript instantiates the t-slot at the enclosing proposition's s in [8 gamma, 1/2]. The interval (1/4, 1/2] is not covered. Ugly.uglyJEstimate_of_sensitivity itself is stated on the full [8 gamma, 1/2] window, so a future producer of the four-term bound valid there composes with no change.

The gapped gauge

The right-hand side Cl * 3^{gamma(m-n)} is unchanged. See UglyPre.

The sigmaBar_{n-2} lower constant

The sigmaBar_{n-2} lower bound is carried at 1/4, not at the printed 1/2: the Section 3 induction state supports only the relaxed constant at the exponent 3^{gamma n}. See Ugly.lean for the arithmetic and for the resulting constant bookkeeping in the hC slot.

theorem Algsuperdiff.Section4.Provider.Annular.exists_responseJ_ugly_estimate (d : ℕ) (dimension : 2 ≤ d) : ∃ (Cs : ℝ), 0 < Cs ∧ ∀ (M : Section3.ABKModel d) (m n : ℤ) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (e : HCPolySupport.Vec d) (s kap Cl Cr Cp Ash C Gn Gm Lnrm : ℝ), 0 < s → s ≤ 1 / 4 → 8 * M.gamma ≤ s → HCPolySupport.Book.Ch02.vecNorm e = 1 → ↑n ≤ ↑m → 0 ≤ Ash → 0 ≤ Gn → 0 < kap → M.gamma * kap ^ 2 = Section3.Disorder.cstar M → 1 / 2 * (kap * 3 ^ (M.gamma * ↑m)) ≤ ↑(Section3.Annealed.sigmaBar M m) → 1 / 4 * (kap * 3 ^ (M.gamma * ↑n)) ≤ ↑(Section3.Annealed.sigmaBar M (n - 2)) → ↑(Section3.Annealed.sigmaBar M (n - 2)) * (Frozen.Section24.unitCubeLambda (2 * M.gamma) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ Cl * 3 ^ (M.gamma * (↑m - ↑n)) → (↑(Section3.Annealed.sigmaBar M (n - 2)))⁻¹ * (3 ^ (2 * ↑n) * Gn) ≤ Ash * 3 ^ (s / 4 * (↑m - ↑n)) → (↑(Section3.Annealed.sigmaBar M m))⁻¹ * ↑(Section3.Annealed.sigmaBar M (n - 2)) ≤ Cr → h.gradientW1Infinity = 3 ^ (2 * ↑n) * Gn → h.valueL2 ^ 2 ≤ 2 * Lnrm ^ 2 + 2 * (Cp * (3 ^ (2 * ↑m) * Gm)) ^ 2 → Cs * (1 + Ash * Cl) ^ 2 * Cr * (1 + Cl) + 16 * Cs * (1 + Ash * Cl) ^ 2 * Cl * (1 + Cp ^ 2) + 4 * Cs * (1 + 4 * Cl ^ 2) ≤ C → IsUglyJEstimate (HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn 1) (Section3.Observable.inverseSqrtLoad (Section3.Annealed.sigmaBar M m) e) (Section3.Observable.sqrtLoad (Section3.Annealed.sigmaBar M m) e)) (Frozen.Section24.unitCubeHomogenizationError s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (n - 2))) ^ 2) ((↑(Section3.Annealed.sigmaBar M m) * (↑(Section3.Annealed.sigmaBar M (n - 2)))⁻¹ - 1) ^ 2) ((3 ^ (-(M.gamma * ↑n)) * Lnrm) ^ 2) ((3 ^ ((2 - M.gamma) * ↑n) * Gn) ^ 2) ((3 ^ ((2 - M.gamma) * ↑m) * Gm) ^ 2) (Section3.Disorder.cstar M) M.gamma (3 ^ (s * (↑m - ↑n))) (3 ^ ((s + M.gamma) * (↑m - ↑n))) C

The composed per-cube estimate: the unconditional sensitivity anchor, at the (mu, sigma_0)-witness, collapsed by the two good-event budgets, the two sigmaBar lower bounds, the sigmaBar ratio and the Poincare split into the printed five-term display.