RootClauseBDichotomyDisplay

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

an abstract fine-side hgrad — NO coarse gate

Nothing here imports any of them, nothing here claims an anchor, and nothing here is a frozen statement.

The item

• the coarse side at the print's own well-placed re-based frame (units A--C, F): the ONLY geometric inputs are z ∈ □_m and the scale ladder;
• the fine side abstracted into the chain's hgrad slot, so the fine-scale dichotomy (GATE(n') / flush(n'), both branches proved) can feed it;
• the dataM slot abstract, priced by the caller on the printed carrier √σ_m^{-1}·3^{m/2}K_g — so BOTH branches (the gated Caccioppoli's dataM and the flush branch's priced 𝐠-legs) enter one display.

The conclusion is the boundary three-leg display V (the printed √σ_m·3^{m/2}K_h leg included), at every centre z ∈ □_m.

References

• ABK26, t.regularity; Step 7.

1. The well-placed prefactor

noncomputable def Algsuperdiff.Section4.Provider.Regularity.rootClauseBWellPlacedPrefactor (d : ℕ) (Cch Cg CB Ctr CWG CWH CdM : ℝ) : ℝ

The well-placed boundary prefactor: the collapse constant of the display below.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseBWellPlacedPrefactor_nonneg (d : ℕ) {Cch Cg CB Ctr CWG CWH CdM : ℝ} (hCch : 0 ≤ Cch) (hCg : 0 ≤ Cg) (hCB : 0 ≤ CB) (hCtr : 0 ≤ Ctr) (hCWG : 0 ≤ CWG) (hCWH : 0 ≤ CWH) (hCdM : 0 ≤ CdM) : 0 ≤ rootClauseBWellPlacedPrefactor d Cch Cg CB Ctr CWG CWH CdM

The well-placed prefactor at nonnegative data.

2. The display

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseB_display_wellPlaced_of_hgrad (d : ℕ) [NeZero d] : ∃ (Cch : ℝ), 0 < Cch ∧ ∀ (M : Section3.ABKModel d) (m0 : ℤ) (Ecap : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Ecap → M.gamma < 1 / 2 → ∀ (L : ℤ) {alpha : ℝ} {n m kc np : ℤ} {z : HCPolySupport.Vec d} (omega : Section3.Cutoff.CutoffSample d) (uglob hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} {Khol Kh Kd CB Cg Cdel CdM CWH C1 delta Cest dataH dataM : ℝ} {B : ℕ}, z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → m ≤ m0 → n ≤ m → kc ≤ m - 1 → np + 1 ≤ m → m - (kc + 1) ≤ ↑B + 1 → Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) uglob hdat gsrc → MeasureTheory.MemLp gsrc 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 gsrc) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → 0 ≤ Khol → 0 ≤ Kh → 0 ≤ Kd → 0 ≤ CB → 0 ≤ Cg → 0 ≤ Cdel → 0 ≤ CdM → 0 ≤ CWH → 0 ≤ dataH → 0 ≤ dataM → 2 * ↑d + 2 ≤ C1 → 0 ≤ alpha → alpha ≤ 1 → delta ≤ C1⁻¹ * (1 - alpha) → ↑B ≤ delta * (↑(m - n).toNat + 1) → stepSevenCgLamInv (HCPolySupport.originCube d kc) (ExcessDecay.parentRebasedFamily M L (kc + 1) (ExcessDecay.wellPlacedCentre z m kc) z omega) stepSevenCgS ≤ CB * (↑(Section3.Annealed.sigmaBar M (kc + 1)))⁻¹ → (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d kc) stepSevenCgS fun (x : HCPolySupport.Vec d) => -gsrc (x + ExcessDecay.wellPlacedCentre z m kc)) ≤ Kd * edFinalDataOscG Khol m → dataM ≤ CdM * (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * edFinalDataOscG Khol m) → dataH ≤ CWH * edFinalDataOscG Kh m → stepSevenNuGradNorm M.nu (ExcessDecay.truncatedWindow z m (n + 1)) uglob.grad ≤ Cg * √↑(Section3.Annealed.sigmaBar M (np + 1)) * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * ((HCPolySupport.cubeScaleFactor (HCPolySupport.originCube d kc))⁻¹ * Support.normalizedL2On (ExcessDecay.truncatedWindow z m kc) fun (x : HCPolySupport.Vec d) => uglob.toFun x - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m kc) uglob.toFun) + Cg * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√↑(Section3.Annealed.sigmaBar M (np + 1)) * (1 * ⋯) + dataM) → rootClauseBWellPlacedPrefactor d Cch Cg CB (rootClauseBTopCtr d Kd) (edFinalDataOscW M Cdel * stepFourGagliardoConst d stepOneS) CWH CdM ≤ Cest → (√M.nu * Support.normalizedL2On (ExcessDecay.truncatedWindow z m (n + 1)) fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (uglob.grad y))) ≤ Cest * Real.rpow 3 ((1 - alpha) * (↑m - ↑n)) * ((√M.nu * Support.normalizedL2On (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (uglob.grad y))) + ⋯ * Khol + √↑(Section3.Annealed.sigmaBar M m) * Real.rpow 3 (↑m / 2) * Kh)

Clause (A) of the a.e. lattice display at the W frame, from the fine-side hgrad — no coarse gate, every centre z ∈ □_m. See the module docstring.