BoundaryCoveringSlot #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The boundary lane's covering cube, read at the slot n+3 #
CoveringSlotObstruction measured exactly this: on the
boundary branch the covering cube c + □_{n+2}, c = wellPlacedCentre x m (n+2), leaves the n+2 good-event slot's cube, and always sits inside
the n+3 one. The frozen general clause puts its slot at
n+3 precisely so that this positive half is usable. This module cashes
it in, at the level the boundary Caccioppoli step consumes.
Three steps, each proved elsewhere and composed here:
- the half-open containment —
CoveringSlotObstruction's open-cube containmentc + □_{n+2} ⊆ z + □_{n+3}re-derived in the half-open realization the off-grid transports require (the margin is ample: the centre moves by less than6·3^nand the half-open child reaches4.5·3^n, against the parent's13.5·3^n); - the off-grid transport at depth
1—OffGridErrorFluxCorrected's root transport atK = □_{n+3},P = □_{n+2}, so the depth factor is a single3^{u·1}, i.e.3^{s/8} ≤ 3^{1/8} < 1.15; - the good event at the
n+3slot —ReindexSlot's(n+3)caps, read atL ≥ n+3(the frozen bindern + 3 ≤ m ≤ L).
No antisymmetric-shift conversion is used: nothing below converts Λ or λ
by the antisymmetric-shift invariance. The whole chain runs at the (n+3)
family parentRebasedFamily M L (n+3) c z ω — the covering cube's own frame
at the parent's constant — which is the family InteriorRebase builds and the
one the equation transports to for free.
The q = 1 ingredients are supplied here, at the covering cube:
CaccioppoliInteriorPrefactor's constant-1 comparisons Λ_{u,1} ≤ Λ_{u/2,2}
and λ_{u,1}^{-1} ≤ λ_{u/2,2}^{-1} turn the q = 2 ratio cap into the q = 1
ingredients Λ_{u,1}, λ_{u,1}^{-1} and Θ that
caccioppoliWithRHSPrefactor reads.
What this does not do #
It does not prove the boundary clause. The boundary lane still needs its
analytic half (the trace-measure Poincaré and the Stampacchia step), the
boundary energy assembly at this family, and the L²/window transport onto the
general clause's window. Nothing below is an instance, or a fraction, of any
source node.
References #
- ABK26,
e.mathcalE.stability.applied; the boundary application ofl.coarse.grained.Caccioppoli.RHS.
1. The half-open containment of the covering cube in the n+3 parent #
Displacement control places the clamped covering cube in its anchor parent.
The covering cube inside the n+3 parent, half-open.
2. The off-grid transport at depth one #
The covering cube's coarse-graining error against the general clause's representative.
At every index t strictly above the good-event index s/8 and at most 1/2,
the covering cube's q = 2 error at the (n+3) re-based family is bounded by
the frozen clause's own fluxCorrectedErrorRepresentative M L (n+3) ⟨s/8⟩,
with the depth-one factor 3^{s/8} (at most 3^{1/8} < 1.15).