ResidueBudget #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The residue budget form of the boundary scalar, and the sharpening record #
What is proved #
Two consequences of ResidueInterface.exists_scalarControl_boundaryBranch_
comparator.
exists_scalarControl_of_boundaryBranch_harmonicResidue— the∀-budget form. For any realRthat dominates‖u − w‖_{L²(K')}for everyΔ-harmonic comparatorw = u + ρ,ρ ∈ H¹₀(K'), the boundary scalar obeysS ≤ C(d)·( ‖u − (u)_{W'}‖_{L²(W')} + 3^n·Σᵢ‖∂ᵢh‖_{L²(W')} + R ) .This is the shape the boundary assembly consumes;
Ris a caller obligation and is disclosed as such.exists_scalarControl_of_boundaryBranch_recovered— the sharpening record: instantiating the budget by the Dirichlet-principle Poincaré bound ofSealComparatorreturns, verbatim in shape, the proved composed scalar theorem of the boundary lane's seal chain (at the constantC·max 1 (comparatorPoincareConst d)). Nothing is lost by moving to the comparator interface.
Why the interface was moved #
The gradient residue 3^n·Σᵢ‖∂ᵢu‖_{L²(K')} has exactly two known producers and
both are blocked:
- the fitted boundary Caccioppoli of
SealCaccioppoliGeometryprices theν-weighted energyν·⨍_{K'}|∇u|², so extracting the Euclidean gradient costs√(σ/ν); - the
p = 2general coarse-graining comparison prices the comparator distance directly, but at the envelope factors^{-4}·𝓔.
The second producer does not price the gradient at all; it prices
‖u − w‖_{L²(K')}. Moving the interface to ‖u − w‖ is therefore what makes
that producer even expressible. Its arithmetic is measured in
ResidueAbsorption.lean.
References #
- ABK26,
l.harmonic.approximation.good.scales, Step 2.
The sum of coordinate L² norms is bounded by dimension times the vector L² norm.
1. The ∀-budget form #
The boundary scalar at an abstract residue budget.
R is any real dominating the harmonic-approximation error at the flush
sub-cube K' for every Δ-harmonic comparator of u there.