BoundaryClauseSkeleton #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The boundary Caccioppoli's L² object, reduced to the escalated scalar #
S₀ = |(u − h)_{c + □_{n+2}}| , c = wellPlacedCentre x m (n+2) ,
This module carries out the composition parametrized by that scalar: with
S an abstract bound for it, the boundary Caccioppoli's L² object splits
into three frozen shapes plus S,
‖u(·+c) − V‖_{L²(□_{n+2})}
≤ 2·3^d ‖u − (u)_{W'}‖_{L²(W')} (the FIRST leg)
+ C(d)·3^{n+2}·3^d Σᵢ ‖∂ᵢh‖_{L²(W')} (the FIFTH leg shape)
+ S (the escalated scalar)
+ ‖σ‖_{L²(□_{n+2})} , (the σ leg)
W' = (z+□_{n+3}) ∩ □_m, σ = V − h(·+c) ∈ H¹₀(□_{n+2}).
The disclosed slot #
S enters the conclusion additively, in its own leg, at coefficient 1.
That is the honest reading: the scalar is an additive normalization defect of the
L² object, not a multiplier of any datum. A producer supplying
hmean at some S together with a bound of S by the frozen bracket closes the
composition at twice the constant; a producer supplying S = 0 closes it by
add_zero.
What remains after this module #
Exactly two inputs, both already named:
- the
σ-leg choice —BoundaryGradHsection 4's fork, i.e. whether theν-division is authorized.
References #
- ABK26,
l.harmonic.approximation.good.scales, Step 2;l.coarse.grained.Caccioppoli.RHS.
1. Jensen in the normalized carrier #
2. The mean-zero Poincaré on the boundary covering cube #
The equal-sides mean-zero cube Poincaré on c + □_j ⊆ □_m.
The c-and-scale-generic form of BoundaryClauseSkeleton's covering-cube
instance: any translated origin cube inside □_m is an axis cube of side
3^j, and CoarseGraining's scale-uniform mean-zero Poincaré applies verbatim;
the normalization cancels because the same cube carries both sides.
The mean-subtracted L² Poincaré inequality on the covering cube.
The covering cube c + □_{n+2} is an axis cube of side 3^{n+2}, so
CoarseGraining's scaled mean-zero Poincaré applies verbatim; the normalization
cancels between the two sides because the same cube carries both.