ResidueCapGeometry #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The three geometric hinges of the boundary cap chain, verified at the flush #
sub-cube K' #
Nothing here imports that file, and nothing here claims the anchor or any source node.
What is proved #
ResidueAbsorption.exists_flushSubCube_not_subset_anchorGeometry shows that
the flush scale-n sub-cube K' = flushSubCentre z m n i σ + □_n provably
fails the anchor's geometry binder x + □_n ⊆ (z+□_{n+1}) ∩ □_m on a genuine
3·3^n-wide far-range of the boundary branch. That block is a statement about
binders. This module measures what the proved boundary cap chain actually
consumes from that binder, and discharges each item at K' from the anchor's
own (n+3, z) frame instead.
Three hinges — and only three — carry hgeom through the whole chain:
(W) wellPlacedCentre x m (n+2) + □_{n+2} ⊆ (z+□_{n+3}) ∩ □_m
(`image_add_wellPlacedCentre_subset_anchorWindow`; the window
transports `BoundaryTransports`, `BoundaryGradH`,
the parent-`L²` pricing and the energy legs use nothing else)
(P) translateSet (wellPlacedCentre x m (n+2) − z) (cubeSet □_{n+2})
⊆ cubeSet □_{n+3}
(`translateSet_cubeSet_coveringCube_subset_anchorParent`; the covering
cube's error/ellipticity caps use nothing else)
(C) translateSet (x − z) (cubeSet □_n) ⊆ cubeSet □_{n+3}
(`translateSet_cubeSet_subset_of_anchorGeometry` composed with the half-open
nesting; the child cube's error/ellipticity caps use nothing else)
At x := flushSubCentre z m n i σ, (W) is already proved
(SealCaccioppoliGeometry.outer_subset_anchorWindow_flushSubCentre item 4),
and (P), (C) are proved here. The margin is real, not tight: the flush
sub-centre sits at |c'ᵢ − zᵢ| ≤ 8.5·3^n against the 13·3^n the (n+3)
frame allows, and the clamp defining the covering centre cannot increase that
distance (§1).
References #
- ABK26,
l.harmonic.approximation.good.scales, Step 2.
1. The clamp cannot move a centre away from a nearby reference point #
The covering clamp, measured against a reference point.
wellPlacedCentre a m k is the coordinatewise clamp of a into
[−A, A], A = ½3^m − ½3^k. If a reference point b lies in □_m and aᵢ is
within D of bᵢ for some D ≥ ½3^k, then the clamped coordinate is still
within D of bᵢ: clamping either does nothing, or moves aᵢ towards the
origin and therefore towards b, and the residual is at most the clamp gap
½3^k.
The flush sub-centre stays within 8.5·3^n of z.
c' = wellPlacedCentre z m (n+2) pushed by ½(3^{n+2} − 3^n) = 4·3^n in the
σeᵢ direction: the clamp contributes at most ½3^{n+2} = 4.5·3^n and the push
exactly 4·3^n.
3. Hinge (C): the child cube inside the (n+3) parent, half-open #
Hinge (C) at K'.
K' − z + □_n ⊆ □_{n+3} in the half-open realizations: 8.5·3^n + 0.5·3^n = 9·3^n against the available 13.5·3^n. This is the containment the proved
off-grid transport
OffGridErrorFluxCorrected.ae_offGridErrorFunctional_le_fluxCorrectedErrorFunctionalAtRoot
consumes, read at the root □_{n+3}.
4. Hinge (P): the covering cube of K' inside the (n+3) parent #
Hinge (P) at K'.
The covering centre wellPlacedCentre c' m (n+2) is still within 8.5·3^n of
z (§1, at D = 8.5·3^n ≥ 4.5·3^n = ½3^{n+2}), so the covering cube's
half-open realization sits inside □_{n+3}: 8.5·3^n + 4.5·3^n = 13·3^n
against the available 13.5·3^n. This is the containment
BoundaryCoveringSlot.ae_coveringCubeError_le_representative consumes.
5. The covering centre of K' is the anchor's own flush centre #
The clamp collapses the flush push.
wellPlacedCentre (flushSubCentre z m n i σ) m (n+2) = wellPlacedCentre z m (n+2)
on the boundary branch. Off the i-axis the flush sub-centre already is the
clamped anchor centre, and the clamp is idempotent; on the i-axis the overhang
wellPlacedHalfGap m (n+2) < σ zᵢ puts both zᵢ and the pushed coordinate
strictly beyond the clamp gap on the same side, so both clamp to σ·A.
6. Hinge (W) and the frame containments, collected at K' #
See SealCaccioppoliGeometry.outer_subset_anchorWindow_flushSubCentre.
The flush sub-cube's own frame containment, in the translateSet
spelling the coarse-graining composition consumes.