SealDatumStep #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The datum step of the S4.3 boundary lane, closed on the anchor's own core cube #
What is proved #
Let x, z ∈ □_m, n + 2 ≤ m, and let the anchor's geometry binder
x + □_n ⊆ (z + □_{n+1}) ∩ □_m hold. Write
V₁ := wellPlacedCentre x m (n+2) + □_{n+2} (the anchor's covering cube)
K := wellPlacedCentre z m (n+2) + □_{n+2} (the boundary-flush cube)
W' := (z + □_{n+3}) ∩ □_m (the anchor's own window)
and let K' := c' + □_n be any scale-n cube inside K (the intended
instance is the sub-cube flush against the face K shares with ∂□_m). For the
anchor's Dirichlet datum h : H1Function □_m this module proves, with no
hypothesis beyond those binders,
|⨍_{V₁} h − ⨍_{K'} h|
≤ datumStepConst d · 3^n · Σᵢ ‖∂ᵢh‖_{L²(W')} ,
datumStepConst d = 27 · 3^d · 3^d · unitMeanZeroPoincareConst d, i.e. exactly
the frozen fifth-leg shape: a constant depending on d alone, a single factor
3^n, the gradient read on W', no s-power, no σ, no ν.
The mechanism: the anchor's own core cube, not a translation estimate #
The route originally scoped for this step was the H¹ translation estimate
between the two scale-(n+2) cubes V₁ and K (they are translates of one
another). That route needs the fundamental theorem of calculus along lines for a
weak gradient, which exists nowhere in the upstream library. It is not needed.
The anchor's binders already supply a set contained in both cubes, namely the anchor's own core window
J := x + □_n .
Indeed J ⊆ □_m and J ⊆ z + □_{n+1} are two halves of the geometry binder,
so J ⊆ truncatedWindow x m n ⊆ V₁ and J ⊆ truncatedWindow z m (n+1) ⊆ K by
the proved covering lemma truncatedWindow_subset_image_add_wellPlacedCentre
at the scales n ≤ n+2 and n+1 ≤ n+2. Since |V₁| / |J| = |K| / |J| = |K| / |K'| = 9^d, the three mean transfers of MeanControlReduction each cost the
exact factor 3^d, and the chain
|⨍_{V₁}h − ⨍_{K'}h| ≤ |⨍_{V₁}h − ⨍_J h| + |⨍_J h − ⨍_K h| + |⨍_K h − ⨍_{K'}h|
is closed by the equal-sides mean-zero cube Poincaré on V₁ and on K
separately. Both are genuine cubes of side 3^{n+2} sitting inside □_m, so
BoundaryClauseSkeleton.eLpNorm_sub_average_coveringCube_le_meanZeroPoincare
applies verbatim (read at x, and at z). The window W' enters only
through the two proved L² transports at the 3^d volume ratio.
A recorded side fact: the window's eccentricity #
Section 7 records, independently of the chain above, that W' is an
axis-aligned box all of whose edges have length in (½·3^{n+3}, 3^{n+3}] —
i.e. its eccentricity is at most 2, uniformly over every configuration the
anchor's binders allow. Nothing in sections 1--6 consumes it.
0. Volume and integrability slots of a translated origin cube #
The real volume of a translated origin cube.
A translated origin cube has finite volume.
A translated origin cube has positive real volume.
A translated origin cube is measurable.
The datum is L² on every subset of its own domain.
Each coordinate of the datum's weak gradient is L² on every subset of the
datum's own domain.
An L² function on a finite-measure set is integrable there.
The square of a mean-shifted L² function is integrable.
1. The anchor's own core cube sits inside both scale-(n+2) cubes #
The core cube lies in the anchor's covering cube.
x + □_n ⊆ wellPlacedCentre x m (n+2) + □_{n+2}: the anchor's geometry binder
puts x + □_n inside □_m, so it is the truncated window truncatedWindow x m n and the proved covering lemma applies at n ≤ n + 2.
The core cube lies in the boundary-flush cube.
x + □_n ⊆ wellPlacedCentre z m (n+2) + □_{n+2}: the anchor's geometry binder
puts x + □_n inside truncatedWindow z m (n+1), and the proved covering
lemma applies at n + 1 ≤ n + 2.
2. The two-scale volume ratio #
The square root of the volume ratio between a scale-(k+2) cube and a
scale-k cube is exactly 3^d.
3. The two-scale mean transfer on the datum #
The two-scale mean transfer.
For a scale-k cube inside a scale-(k+2) cube, the gap between the two datum
means is at most 3^d times the oscillation of the datum on the big cube.
4. The equal-sides cube Poincaré, in the normalizedL2On spelling #
The mean-zero Poincaré on a well-placed cube, in the real seminorm.
BoundaryClauseSkeleton.eLpNorm_sub_average_coveringCube_le_meanZeroPoincare
read through the normalizedL2On dictionary. The cube is a genuine equal-sides
cube of side 3^{n+2} inside □_m, so the constant is scale-uniform: it is
unitMeanZeroPoincareConst d times the side length.
5. The L² transport of a scale-(n+2) cube onto the frozen window #
The window transport at a general centre.
Any scale-(n+2) cube inside the frozen window W' = (z+□_{n+3}) ∩ □_m prices
its normalized L² norms at the volume ratio 3^d. The volume comparison
volume_anchorWindow_le_coveringCube carries no hypothesis on the centre, so
this serves the x-cube and the z-cube alike.
The coordinate-sum form of the window transport, on the datum's gradient.
6. The datum step #
The datum step's coefficient-free constant: 27 · 3^d · 3^d times the
absolute mean-zero Poincaré constant of the unit cube.
Equations
Instances For
The datum step of the boundary lane.
The two datum means the boundary chain compares — the one on the anchor's own
covering cube V₁ = wellPlacedCentre x m (n+2) + □_{n+2} and the one on any
scale-n sub-cube K' of the boundary-flush cube K = wellPlacedCentre z m (n+2) + □_{n+2} — differ by at most the frozen fifth-leg shape
datumStepConst d · 3^n · Σᵢ ‖∂ᵢh‖_{L²(W')} , W' = (z+□_{n+3}) ∩ □_m .
The proof chains three two-scale mean transfers through the anchor's own core
cube x + □_n, which the geometry binder places inside both scale-(n+2)
cubes, and closes each oscillation by the equal-sides mean-zero cube Poincaré on
V₁ and on K separately. No Poincaré inequality is taken on W', no
translation estimate is used, and no analytic input is assumed.