InteriorAssemblyAnchorShape #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The anchor-shape weakening of the correction leg #
The composed correction leg of InteriorGlue is stronger than the frozen
statement's second interior summand: it carries the honest s^{-1/2} where the
anchor prints s^{-7}, and the honest σ_{n+2} where the anchor prints σ_n.
This module records the weakening, so that the composed estimate can be read
in the anchor's own printed shape:
σ_{n+2}^{-1} · 3^{n} · (correction leg)
≤ C(d) · s^{-7} · σ_n^{-1} · 3^{(1+s)n} · [g]_{H^s(x+□_n)} ,
which is exactly the frozen statement's
C s^{-7} σ_n^{-1} 3^{(1+s)n} [g]_{H^s(W)}
with C = 4 · interiorCorrectionConst d. Two steps, both priced and both
one-directional:
- the
σindex moveσ_{n+2}^{-1} ≤ 4 σ_n^{-1}—SigmaBarIndex, discharged inside the anchor's own regime, no landmark binder.
The prefactor σ_{n+2}^{-1} · 3^{n} is exactly what dividing the harmonic
display of the child-frame composition by its own left-hand weight
σ · cubeBesovScaleWeight 1 (□_n) = σ · 3^{-n} produces, at the comparator
choice σ := σ_{n+2} (the index of the parent's flux correction and of the
anchor's error slot).
No γ-move is made anywhere; the regime is the anchor's own
γ ≤ C^{-1} c⋆^{10}.
References #
- ABK26,
l.harmonic.approximation.good.scales, (the interior clause's second summand).
1. The two one-directional moves #
The anchor's geometry binder, in the translateSet spelling the child-frame
composition is entered at.
Restrict clause-(iv) data to the frontier-empty parent window and its child. The result is independent of the coefficient slot used by the comparison.