ResidueScalarFlush #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The boundary scalar at the flush covering cube, at the residue interface #
Nothing here imports that file, and nothing here claims the anchor or any source node.
What is proved #
ResidueInterface.exists_scalarControl_boundaryBranch_comparator prices the
anchor's own scalar |⨍_{V₁}(u−h)|, V₁ = wellPlacedCentre x m (n+2) + □_{n+2}.
K = wellPlacedCentre z m (n+2) + □_{n+2} .
exists_scalarControl_flushCube_comparator is the same estimate read at K:
|⨍_K (u−h)| ≤ C(d) · ( ‖u − (u)_{W'}‖_{L²(W')}
+ 3^n · Σᵢ ‖∂ᵢh‖_{L²(W')}
+ ‖u − w‖_{L²(K')} )
for the produced Δ-harmonic comparator w = u + ρ, ρ ∈ H¹₀(K'), together
with the ∀-budget form exists_scalarControl_flushCube_harmonicResidue.
This is the exact statement that closes the S-loop of route 1: the
composition's S-companion is bounded by the composition's own legs plus its
own left-hand side.
References #
- ABK26,
l.harmonic.approximation.good.scales, Step 2.
1. The scalar at the flush cube, with the comparator produced #
The boundary scalar at the flush cube K, with the residue exhibited as
the harmonic-approximation error at K'.
The binder-free sibling of
ResidueInterface.exists_scalarControl_boundaryBranch_comparator: the
anchor's geometry binder and its child centre x do not occur.
2. The ∀-budget form #
The boundary scalar at the flush cube, at an abstract residue budget.
R is any real dominating the harmonic-approximation error at K' for every
Δ-harmonic comparator of u there. This is the form the route-1 loop
consumes.