CoarseAssemblyBudget #

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

The boundary assembly's square root, its scaled `L²` object, and its #

Nothing here imports that file, and nothing here claims the anchor or any source node.

What is proved #

§1 — the square root of the boundary Caccioppoli's display. The general-data boundary Caccioppoli of CoarseAssemblyDatum is a squared display; the assembly consumes its square root. The step is pure real arithmetic and is stated on abstract letters so that no cube, measure or coefficient field enters.
The two 3-powers cancel on the data-Poincaré leg, and the open scalar S survives at coefficient 3^{-(n+2)} — which the frame division later turns into the pure constant 3^{-2}, so S carries no 3-power in the final display.

The `s`-powers, in words #

With the proved envelope's s^{-4} on the coarse-graining energy term (ReindexEllipticity.eLpNorm_sub_weaklyHarmonic_le_coarseGraining_rebased_addThree) and the r = s/2 pin of the fidelity plan:

  direct Dirichlet-energy ∇h leg     s^{-4} · (s/2)^{-1/2}                 = 2^{1/2} · s^{-9/2}
  direct Dirichlet-energy [g] leg    s^{-4} · (s/2)^{-3/2}                 = 2^{3/2} · s^{-11/2}
  datum pricing, crude leg           s^{-4} · s^{-1/2}                     = s^{-9/2}
  datum pricing, force leg           s^{-4} · (s/2)^{-3}                   = 2^3 · s^{-7}
  datum pricing → DirE [g] leg       s^{-4} · (s/2)^{-3/2} · (s/2)^{-3/2}  = 2^3 · s^{-7}
  datum pricing → DirE ∇h leg        s^{-4} · (s/2)^{-3/2} · (s/2)^{-1/2}  = 2^2 · s^{-6}

The frozen legs are s^{-4} (first), s^{-7} (force), s^{-9/2} ([∇h] seminorm) and s^{-9/2} (‖∇h‖_{L²}). The first five rows land; the sixth does not, and §4 shows it cannot be made to.

References #

ABK26, l.coarse.grained.Caccioppoli (move 3); the boundary application; l.harmonic.approximation.good.scales.

1. The square root of the boundary Caccioppoli display #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_le_of_boundaryCaccioppoliDisplay {LCE D3 P Lam T2 Nsq E18 DirE : ℝ} (hD3 : 0 ≤ D3) (hP : 0 ≤ P) (hLam : 0 ≤ Lam) (hT2 : 0 ≤ T2) (hNsq : 0 ≤ Nsq) (hE18 : 0 ≤ E18) (hDirE : 0 ≤ DirE) (h : LCE ≤ D3 * (2 * (P * (Lam * T2 * Nsq)) + 2 * (E18 * DirE ^ 2))) :

√LCE ≤ √(2 * D3 * (P * Lam)) * (√T2 * √Nsq) + √(2 * D3 * E18) * DirE

The square root of the boundary Caccioppoli's squared display.

  3^d ( 2 · pref · (λ_t · 3^{-2(n+2)} · N²) + 2 · 18^d · DirE² );

the assembly consumes the square root of the left-hand side. Stated on abstract letters: D3 = 3^d, P = pref, Lam = λ_t, T2 = 3^{-2(n+2)}, Nsq = N², E18 = 18^d.

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeBesovScaleWeight_one_originCube_eq {d : ℕ} (k : ℤ) :

HCPolySupport.cubeBesovScaleWeight 1 (HCPolySupport.originCube d k) = Real.rpow 3 (-↑k)

The covering cube's Besov scale weight is the frame factor 3^{-(n+2)}.

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.rpow_three_neg_mul_zpow_self (k : ℤ) :

Real.rpow 3 (-↑k) * 3 ^ k = 1

The frame factor cancels the covering cube's own diameter.

2. The scaled parent-`L²` object of the boundary Caccioppoli #

source

Real.rpow 3 (-↑(n + 2)) * √(HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) fun (y : HCPolySupport.Vec d) => utr.toFun y - v.toH1.toFun y) ≤ Real.rpow 3 (-↑(n + 2)) * (3 ^ d * (MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal) + Real.rpow 3 (-↑(n + 2)) * S + HCPolySupport.unitMeanZeroPoincareConst d * (↑d * (3 ^ d * (MeasureTheory.eLpNorm hdat.grad 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal)) + R

4. The Dirichlet energy right-hand side, at the hinge #

source

The parent-L² pricing, scaled by the covering cube's frame factor.

Two readings of the conclusion matter for the assembly:

the data-Poincaré leg loses its 3-power entirely (3^{-(n+2)} · 3^{n+2} = 1), so after the frame division it proves at the frozen leg's 3^n;
the open scalar S survives at coefficient 3^{-(n+2)} and at coefficient 1 in S itself, so after the frame division it is 3-power-free.

source