ResidueDatumFlush #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The datum step at the flush pair (K, K') #
Nothing here imports that file, and nothing here claims the anchor or any source node.
What is proved #
SealDatumStep.abs_volumeAverage_datum_sub_le_datumStep compares the datum's
mean on the anchor's covering cube V₁ = wellPlacedCentre x m (n+2) + □_{n+2}
with its mean on a scale-n cube inside the boundary-flush cube
K = wellPlacedCentre z m (n+2) + □_{n+2}, in three two-scale transfers
(V₁ → x+□_n → K → K'), and needs the anchor's geometry binder to place the
intermediary x + □_n inside both scale-(n+2) cubes.
At the flush pair the intermediary is unnecessary: K' ⊆ K is the proved
flushSubCube_subset_flushCube, so one transfer suffices and the geometry
binder disappears. The output constant is datumStepConst d unchanged (the
one-transfer bound is datumStepConst d / 3 and is weakened to datumStepConst d so the downstream arithmetic is the proved one).
References #
- ABK26,
l.harmonic.approximation.good.scales, Step 2.
The datum step, at the flush pair.
|⨍_K h − ⨍_{K'} h| ≤ datumStepConst d · 3^n · Σᵢ‖∂ᵢh‖_{L²(W')}, from the single
two-scale mean transfer K' ⊆ K, the equal-sides Poincaré on K, and the
binder-free window transport K ⊆ W'.