ShellScalarPriced #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The boundary scalar S, priced: the residue leg discharged #
What is proved #
exists_boundaryScalar_le_displayLegs_of_epsPin: on the boundary branch, the
scalar
S = |⨍_{V₁}(u − h)| , V₁ = wellPlacedCentre z m (n+2) + □_{n+2} ,
obeys, for a.e. sample, on the good event and under the ε-pin
A·𝓔 ≤ s⁴,
S ≤ K · ( ‖u − (u)_{W'}‖_{L²(W')} (the FIRST leg)
+ 3ⁿ · Σᵢ ‖∂ᵢh‖_{L²(W')} (the FIFTH leg)
+ s^{-6}·3ⁿ·‖∇h‖_{L²(W')}
+ s^{-6}·3^{(1+s)n}·[∇h]_{Hˢ(W')}
+ s^{-7}·σ_{n+3}⁻¹·3^{(1+s)n}·[g]_{Hˢ(W')} ) ,
with W' = (z+□_{n+3}) ∩ □_m the frozen window and K explicit. No gradient
residue appears on the right-hand side.
Why this module exists #
The boundary lane's chain prices S with a
third leg 3ⁿ·Σᵢ‖∂ᵢu‖_{L²(K')} — the Euclidean gradient at the flush scale-n
sub-cube — which has no legal producer: the fitted boundary Caccioppoli's
left-hand side is the ν-weighted energy, so extracting the Euclidean gradient
costs √(σ/ν). ResidueScalarFlush re-cuts the scalar theorem so that the
residue becomes the harmonic-approximation distance ‖u − w‖_{L²(K')}
(ResidueScalarFlush.exists_scalarControl_flushCube_harmonicResidue), and
ResiduePlugin prices that residue on the display's own four legs
(ResiduePlugin.exists_flushResidue_le_displayLegs_of_epsPin). The two
have never been composed into a residue-free statement about S itself: the
proved compositions (StitchDisplayLegs, StitchDisplayLegsErrorWeighted) price the
display's S-leg s^{-4}·𝓔·S, i.e. S multiplied by the flux factor,
which is what the frozen theorem's own assembly consumes.
The t.regularity Step-7 shell route needs S bare: the mean gap enters
‖u(·+c) − v‖_{L²(□_k)} at the same weight as the first leg, with no 𝓔
factor available to help. This module supplies exactly that.
The scale the Step-7 shell consumes #
The shell route runs
BoundaryOuterAssembly.exists_boundaryWindowEnergy_le_dirichletDatumRHS at
k := n+3, x := z, c := wellPlacedCentre z m (n+3), so the
mean gap it must kill sits on c + □_{n+3}. That is this theorem's V₁ after
the instantiation n ↦ n+1: the covering cube becomes wellPlacedCentre z m (n+3) + □_{n+3}, the flush sub-cube sits at scale n+1, the window at
(z+□_{n+4}) ∩ □_m, and the good event and the pin are read at (n+4, z).
The overhang costs nothing there: wellPlacedHalfGap m k is decreasing in
k, so the boundary branch's own wellPlacedHalfGap m (n+2) < σ zᵢ already
implies the instantiated wellPlacedHalfGap m (n+3) < σ zᵢ. What the
instantiation does cost is n + 4 ≤ m, the good event and the pin one triadic
scale deeper, and the window read at (z+□_{n+4}) ∩ □_m; those are the
consumer's to supply and are NOT claimed here.
Why the print does not have to do this #
Move 3 of l.coarse.grained.Caccioppoli.RHS does absorb the datum internally:
‖v‖_{L²(□₀)} is bounded by the two printed data legs alone, using v − h ∈ H¹₀(□₀) and the lemma's standing hypothesis (h)_{□₀} = 0. But that
hypothesis is a normalization of h, while Step 2 of
l.harmonic.approximation.good.scales normalizes u instead ("by
subtracting (u)_{(x+□_{n+1})∩□_m} from u"). The shift freedom (u,h) ↦ (u+a, h+a) is ONE scalar and the two normalizations are TWO conditions; their
difference is exactly S. The printed Step 2 sets it to zero silently.
References #
- ABK26,
l.coarse.grained.Caccioppoli.RHS(statement, move 3);l.harmonic.approximation.good.scales, Step 2;t.regularityStep 7.
1. The composition arithmetic #
2. The boundary scalar, priced with no gradient residue #
The boundary scalar S, priced on five legs, residue-free.
S = |⨍_{V₁}(u − h)| at the anchor's own covering cube is bounded by the
frozen first leg, the frozen fifth leg, and the three tail legs of the display,
under the pin A·𝓔 ≤ s⁴ with A produced by the theorem. The Euclidean
gradient residue of the earlier chain — the ν-division that has no legal
producer — does not occur.