StepFourBoundaryJoinDatumSplitErrorWeighted #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The error-weighted Step-4 slot at every centre, and its budget seam #
Nothing here imports the frozen file, nothing here claims the anchor, and nothing here is a frozen statement.
What this module proves #
excessDecay_stepFour_slot_allCentres_datumSplit_errorWeightedβexcessDecay_stepFour_slot_allCentres_datumSplitat the error-weighted clause: the Step-4 slot with no geometric hypothesis at all, at every centre including the boundary lattice centres where the cube gate fails, with the printed datum leg and with theπ-multiplied flatβhleg in theΞ΄slot. The disjunction is discharged byRootInterfaceGate.gate_or_exists_meetsFace.edBridgeDeltaErrorWeighted_le_stepFourDeltaOutErrorWeightedβ the seam: the excess-decay lane's ownΞ΄is bounded bystepFourDeltaOutErrorWeighted's own dominations. The proof isedBracket_le_errorWeightedread atOsc = 0β the bridge'sΞ΄is precisely the collapse's bracket with the oscillation half already spent against the excess (that is what residue 2 does inside the slot), so no leg is double-counted.edBridgeDatumLeg_at_flatIndexβ the datum leg at the budget's own3^{n/2}weight:edBridgeDatumLeg d Cs k n K_h = (C_leg Β· 3^{1/2}) Β· (3^{n/2} Β· K_h). The slot is delivered atj = n+1while the collapse'sΞ΄is indexed atn; the single3^{1/2}is that one-scale offset, and it moves only theA^hconstant.edBridgeDeltaErrorWeighted_add_datumLeg_le_boundaryThreeLegsβ the two composed: the slot's wholeΞ΄-side proves the three-leg grouping `A^g_n- (A^h_n + Ξ΅_j H)
with theA^hconstant widened fromC_bdtoC_bd + C_legΒ·3^{1/2}and **no**Ξ΅`-free flat summand at all.
- (A^h_n + Ξ΅_j H)
References #
- ABK26,
l.excess.decay.good.scales;t.regularitySteps 4--5.
1. The error-weighted Step-4 slot at every centre, geometric half discharged #
The Step-4 decay slot at every printed centre, at the error-weighted clause.
EdBridgeStepFourDatumSplitErrorWeighted.excessDecay_stepFour_slot_general_datumSplit_errorWeighted
with the
join's window disjunction discharged by RootInterfaceGate.gate_or_exists_meetsFace: at
every centre and every scale either the interior gate holds outright, or some coordinate
face of ββ‘_m is met and the carried competitor package supplies the second disjunct. No
interiority, no lattice-centre condition, no gate.
The carried package is asked of the shifted competitor's Weyl representative V,
so it is not forced to vanish on the met face and is chain-satisfiable at a
general Dirichlet datum; the price is the printed datum leg edBridgeDatumLeg
in the Ξ΄ slot.
THE CONSUMPTION SEAM FOR THE ERROR-WEIGHTED Ξ΄.
The excess-decay bridge's own Ξ΄_j at the error-weighted clause is bounded by
stepFourDeltaOutErrorWeighted β the object the collapse produces and the
Ξ±-free boundary budget consumes β through its own dominations and nothing more.
The proof is edBracket_le_errorWeighted read at Osc = 0: the bridge's bracket is
the collapse's bracket with the oscillation half already spent inside the slot
(residue 2 folds it into the contraction and the Ξ΅ |ββ| leg), so setting the
oscillation slot to zero is not a weakening β it is the exact accounting, and
no leg is counted twice.
3. The datum leg at the budget's own index, and the composed budget #
The slot's datum leg at the collapse's 3^{n/2} weight.
The slot is delivered at j = n+1 while the collapse's Ξ΄ is indexed at n;
the single factor 3^{1/2} is exactly that one-scale offset. So as a summand
of the collapse's budget the leg is (C_leg Β· 3^{1/2}) Β· (3^{n/2} Β· K_h) β's
A^h_n shape verbatim, with only the constant moving.
THE BOUNDARY BUDGET AT THE SLOT'S OWN Ξ΄-SIDE.
The whole Ξ΄-side of the error-weighted Step-4 slot β the bridge's Ξ΄ plus the
printed datum leg β sits inside the three-leg grouping
A^g_n + ( A^h_n + Ξ΅_j Β· H ) , H = 2 C_bd K_{h,β} ,
with the A^h constant widened from C_bd to C_bd + C_legΒ·3^{1/2} and
no Ξ΅-free flat summand: the leg priced at Ξ(Ξ³^{-1/2}) is gone, and the
datum leg costs a constant factor on A^h alone.