EdBridgeInteriorClause #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The one-step off the anchor's interior clause (two legs only) #
The anchored interior one-step consumes the anchor's general clause,
which keeps the ∇h terms because the boundary regime needs them. On the
interior branch those terms are dead weight, and worse: the flat ungated leg
C s^{-6} 3^{n-2} ‖∇h‖_{L²} has no decay in n, so its window sum is
(m-n+1)-linear and the Step-5 δ-budget cannot absorb it.
The anchor's second clause — the frontier-empty specialization — carries no
∇h legs at all:
1_{𝒢(n+2,z; s/8, 1/2)} ‖u − v‖_{L²(x+□_n)}
≤ C s^{-4} 𝓔_{n+2} ‖u − (u)_{(z+□_{n+2})∩□_m}‖_{L²((z+□_{n+2})∩□_m)}
+ C s^{-19/2} σ_n^{-1} 3^{(1+s)n} [g]_{H^s((z+□_{n+2})∩□_m)} ,
gated at the bare parent image ((z+□_{n+2}) ∩ ∂□_m = ∅). This module consumes
that clause at the excess-decay window choice and delivers the two-leg
one-step display, which removes that obstruction on the interior branch.
The three indices this route fixes #
At the excess-decay instantiation (anchor index n-2, clamped centre y) the interior clause
reads its event, its flux representative and its display window all at n - 2 + 2 = n:
- the supply event is
𝒢(n, z; s/8, (s/8)√δ)— the printed gate ofl.excess.decay.good.scalesitself, not the general clause'sn+1; - the oscillation leg lives on
(z+□_n) ∩ □_m— the same window the contraction's excess is read on whenx := z, so no window move arises at all on this branch; - the flux representative is at index
n, theσweight and the3-powers atn-2.
The gate, and what it costs #
The clause's gate is on the bare parent image, (z+□_n) ∩ ∂□_m = ∅. It is
strictly stronger than the one-step's own interior gate (x+□_{n-2}) ⊆ □_m (which it implies,
via x ∈ (z+□_{n-3}) ∩ □_m and 3^{n-3}/2 + 3^{n-2}/2 < 3^n/2), and it is
exactly the gate the frozen statement's own design note names: the terminal
consumer supplies it from z ∈ □_{m-1}, matching the manuscript's indicator
1_{z ∉ □_{m-1}}.
The event-free entry #
Nothing about the analysis changes — the event enters the proved chain only
through le_of_indicator_goodEventAt_le, and this module strips the indicator
at its own (printed) index instead of the general clause's.
References #
- ABK26,
l.harmonic.approximation.good.scales, (the anchor; the interior clause);l.excess.decay.good.scales.
1. The two-leg B.toReal expansion #
The two-leg twin of the four-leg B.toReal expansion: the interior
clause's display has no in-bracket companion and no ∇h legs. Unconditional.
2. The event-free interior one-step #
OneStepSchauderComposeInterior.excessDecay_oneStep_interior_of_weaklyHarmonic with its (hmem, hharm)
pair replaced by the bound they exist to produce. The event plays no analytic role in the
chain; stripping the indicator is the caller's business, and this module's caller does it at the
interior clause's own (printed) index.
3. The anchor's interior clause, applied at the one-step window choice #
The anchor's frontier-empty (interior) clause, at the one-step window choice.
Same instantiation as the harmonic-approximation anchor bound — anchor
index n-2, anchor centre the clamped wellPlacedCentre x m (n-2), both
geometric obligations discharged — but the second conjunct is taken. Its event, its
flux representative and its display window all read at n - 2 + 2 = n, and it
carries two legs only: the mean-subtracted oscillation and the force
seminorm. The gate is the frozen statement's own, on the bare parent image.
4. The oscillation fold at the interior clause's window #
** residue 2 at the interior clause's own window — the hOsc slot, T.**
The interior clause reads its oscillation on (z+□_n) ∩ □_m, which at the
excess-decay instantiation x := z is the very window the contraction's excess
is read on. The fold is therefore the proved endpoint comparison with the
3^{-n} normalizer cancelling the window's own 3^n:
3^{-n} ‖u − (u)_{(z+□_n)∩□_m}‖_{L²((z+□_n)∩□_m)} ≤ C_i(d) ( E(u,U_n) + |∇ℓ(u,U_n)| ) .
This is exactly the shape
StepFourCollapseInterface.stepFourDecay_of_edOneStep asks for in its hOsc
binder, at C_osc := endpointConst d (1/9). On the G route the same slot is
not available: there the oscillation lives one scale up, on (z+□_{n+1}) ∩ □_m, and no bound by E(u,U_n) + |∇ℓ(u,U_n)| can hold (a bump supported in
U_{n+1} ∖ U_n leaves the right side unchanged). See
EdBridgeStepFour.oscLeg_normalized_le for the general-clause route's own
(re-indexed) form.
5. The composed two-leg interior one-step #
The interior one-step excess-decay contraction off the anchor's interior clause.
No hharm, no B, no ∇h legs, and — unlike the general-clause route — no
δ re-pricing: the interior clause's own threshold is the frozen 1/2, which
the printed supply event 𝒢(n, z; s/8, (s/8)√δ) reaches from δ ≤ 1 and s ≤ 1 alone.
The two gates are carried separately: hgate is the frozen statement's own frontier-empty
condition on the bare parent image, hcube the one-step's interior inclusion. hgate implies
hcube mathematically (a connected set meeting □_m and missing ∂□_m lies in □_m, and
x + □_{n-2} ⊆ z + □_n from x ∈ z + □_{n-3}); the implication is NOT formalized here — the
connectedness step is a topological detour with no bearing on the display — so both are
hypotheses.