FinalStitch

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

The huglyf slot of clause (i), at the honest frozen event

ABK26, Section 4.1, p.mathcalE.annular.decomp Step 2. UglyLatticeChain.exists_uglyJEstimate_lattice_cube delivers e.ugly.estimate.for.J at one lattice cube 3^n v + □_n and one unit loading e, under seventeen caller obligations. This module composes it into the huglyf binder of ClauseOne.clauseOne_bound — at the annulus maximum over v, at the supremum over e (so that the family matches AssemblyFeed.jLegField, which is the carrier the hpref slot compares against), and with fifteen of the seventeen obligations discharged from proved material and from membership in the honest clause-(i) event

𝒢₁(m; s, √c⋆ γ^{−1/2}) .

What remains, and why

Two obligations are not discharged, and are carried as explicitly named hypotheses. Neither is a proof step migrated into a hypothesis: both are displays the manuscript itself asserts.

• It is carried as a hypothesis here only to keep this module's dependencies at the lattice chain: LambdaBudget it from 𝒢₀(m) and the induction state, at the explicit constant 8(1+9^d)(1+C_cg), and LambdaDischarge discharges the endpoint's slot outright. The binder is stated at the annulus index family Support.latticeAnnulusSet d n m n — the manuscript's own indexing, and a strictly weaker hypothesis than the whole Support.latticeCubeSet d n m. See LambdaBudget's module docstring for the exact uncovered class.
• hsignlow — ¼ κ 3^{γn} ≤ σ_{n−2} (at the relaxed constant). See the discussion in SigmaBarBudget: the induction state gives the printed ½ only with 3^{γ(n−2)}, i.e. short by the factor 3^{2γ}, so ¼ is what the material supports. It is carried as a hypothesis here only to keep this module's dependencies at the lattice chain; SignLowDischarge discharges it outright from the induction state.

Everything else — the two 𝒢₁ budgets, the σ ratio, the σ_m lower bound, the κ normalization, the tail summability, the typing data and the constant inequality — is discharged here, at the explicit constants A_sh = 196, C_r = 4.

Part A -- the two annulus families

@[reducible, inline]

noncomputable abbrev Algsuperdiff.Section4.Provider.Annular.annularResponseMax {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : ℝ

The Jannf family of the clause-(i) composite at the manuscript's own objects: the annulus maximum, over the scale-n lattice cubes of □_j ∖ □_{j−1}, of the scalar response maximum of ã_{L,m}.

This is the same carrier shape as AssemblyFeed.jLegField (a lattice maximum of scalarResponseMax), which is what makes the hpref slot IsAnnularDecompPre s m (jLegField …) (annularResponseMax …) C₁ a comparison of like with like.

Equations

• Algsuperdiff.Section4.Provider.Annular.annularResponseMax M L m omega j n = Algsuperdiff.Section4.Provider.Annular.annularResponseMaxPref M L m omega j n

noncomputable def Algsuperdiff.Section4.Provider.Annular.annularErrorAtomMax {d : ℕ} (M : Section3.ABKModel d) (s : ℝ) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : ℝ

The family at the literal (2,2) annular error atom, i.e. the manuscript quantity rather than the measurable representative. The two agree almost surely (Support.annularErrorAtom_ae_eq_annularErrorObservable); the literal family is what the pointwise chain produces.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Annular.annularResponseMax_nonneg {d : ℕ} (M : Section3.ABKModel d) (L m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : 0 ≤ annularResponseMax M L m omega j n

theorem Algsuperdiff.Section4.Provider.Annular.annularErrorAtomMax_nonneg {d : ℕ} (M : Section3.ABKModel d) (s : ℝ) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : 0 ≤ annularErrorAtomMax M s omega j n

Part B -- the huglyf binder

theorem Algsuperdiff.Section4.Provider.Annular.exists_uglyJEstimate_annulus_of_eventG1 (d : ℕ) (dimension : 2 ≤ d) : ∃ (Cs : ℝ), 0 < Cs ∧ ∀ (M : Section3.ABKModel d) (m L m0 : ℤ) (E : { E : ℝ // 1 ≤ E }) (omega : Section3.Cutoff.CutoffSample d) (s Cl C : ℝ), Frozen.Section3.inductionState M m0 E → m ≤ m0 → m ≤ L → 0 < s → s ≤ 1 / 4 → 8 * M.gamma ≤ s → omega ∈ Support.eventG1 M m s (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹) → 0 ≤ Cl → (∀ (n : ℤ) (v : Fin d → ℤ), n ≤ m - 1 → v ∈ Support.latticeAnnulusSet d n m n → ↑(Section3.Annealed.sigmaBar M (n - 2)) * (Frozen.Section24.unitCubeLambda (2 * M.gamma) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (Section3.Provider.BadEvents.unitRescaledCutoffCoeff M { scale := n, index := v } (n - 2) omega))⁻¹ ≤ Cl * 3 ^ (M.gamma * (↑m - ↑n))) → (∀ n ≤ m - 1, 1 / 4 * (√(Section3.Disorder.cstar M) * (√M.gamma)⁻¹ * 3 ^ (M.gamma * ↑n)) ≤ ↑(Section3.Annealed.sigmaBar M (n - 2))) → Cs * (1 + 196 * Cl) ^ 2 * 4 * (1 + Cl) + 16 * Cs * (1 + 196 * Cl) ^ 2 * Cl * (1 + Section3.Provider.Diffusivity.ApproximateRecurrence.centeringConst d ^ 2) + 4 * Cs * (1 + 4 * Cl ^ 2) ≤ C → ∀ (j n : ℤ), j ≤ m → n ≤ j - 1 → IsUglyJEstimate (annularResponseMax M L m omega j n) (annularErrorAtomMax M s omega j n) ((↑(Section3.Annealed.sigmaBar M m) * (↑(Section3.Annealed.sigmaBar M (n - 2)))⁻¹ - 1) ^ 2) (annularL2Block M m omega j n) (2 * annularGradBlock M m omega j n + 2 * gradTailSq M m omega) (gradTailSq M m omega) (Section3.Disorder.cstar M) M.gamma (3 ^ (s * ↑(m - n))) (3 ^ ((s + M.gamma) * ↑(m - n))) C

e.ugly.estimate.for.J at the annulus, on the honest clause-(i) event.

Of the seventeen obligations of exists_uglyJEstimate_lattice_cube, fifteen are discharged inside: n ≤ m, m ≤ L, the lattice membership, 0 < s, s ≤ 1/4, 8γ ≤ s, ‖e‖ = 1, 0 ≤ A_sh, 0 < κ, γκ² = c⋆, hsigmlow, hshell, hratio, the tail summability, and the constant inequality. The two that remain are hlam and hsignlow (at the relaxed constant ¼, discharged in SignLowDischarge); see the module docstring.