StepFourBoundaryDatumPackage #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The boundary competitor package, and the Step-4 decay at every centre #
What is delivered #
excessDecay_stepFour_slot_allCentres_datumSplit_errorWeighted carries a
disjunction at
every scale: either the interior cube gate z + □_{n-2} ⊆ □_m, or a met face
together with the manuscript's datum-split competitor package (V, v₁, ℓ). At
a boundary lattice centre the gate holds at no scale of the Step-4 chain (a
lattice centre z = 3^n v ∉ □_{m-1} sits at distance ≥ 3^n/2 from ∂□_m, so
the gate fails for every j > n+2 while the chain needs j up to m-1), so
the package branch is the only one available.
This module produces that package from the slot's own moved-cube replacement pair:
truncatedWindow_subset_movedCube_self— theU₂carrier identification at equal index. The inclusion is not "one scale down":truncatedWindow_subset_image_add_wellPlacedCentretakesj ≤ k, so atj = kthe §4.4 window sits inside the anchor's moved cube of the same index. The harmonic domain therefore does transfer, byH1Function.restrict(which sharestoFundefinitionally) andisWeaklyHarmonicOn_restrict.localizedZeroTrace_movedCubeCorrector— theH¹₀corrector of the replacement pair lives on the moved cube, which is strictly larger than the §4.4 window, so it is not anH¹₀(U₂)function; but the odd-reflection glue only ever reads its face-only localized zero trace, andlocalizedZeroTraceFunctionOn_of_memH10_of_inter_subsetsupplies exactly that (reflectedWindow ∩ movedCube ⊆ reflectedWindow ∩ □_m = U₂).exists_datumSplitPackage_movedCubePair— the four package clauses (MemLp V, the packaging identity, the corrector'sL^∞bound, the two face identities, the harmonic class) fromCorrectorComposed'sexists_residualCorrector_affineLift, the affine-split odd competitor, the partial reflection and the harmonic representative.excessDecay_stepFour_decay_allCentres_datumSplit— the slot with the disjunction discharged at every centre.
The one carried input, named exactly #
hgradh : HasGradientOn (truncatedWindow z m (n-2)) h.toFun h.grad.
This is the classical C¹ half of the print's h ∈ C^{1,\nicefrac12}(□_m)
(ABK26 for t.regularity; for l.excess.decay.good.scales), i.e. that
h.grad is the gradient of h and not merely a weak gradient.
AffineSplitLift already treats the pair (HasGradientOn, HolderSeminormBoundOn) as the two halves of h ∈ C^{1,1/2} and carries both.
It is a genuine premise of the printed statement, not a proof step
promoted to a hypothesis.
References #
- ABK26,
t.regularity, (the datumh ∈ C^{1,1/2}(□_m));l.excess.decay.good.scales, (the datum); Steps 4--5.
The U₂ carrier identification, at equal index.
The inclusion is not "one scale down". The proved
truncatedWindow_subset_image_add_wellPlacedCentre takes j <= k, so at j = k the truncated window sits inside the moved cube of the same index.
The reflected window meets the moved cube only inside the truncated window.
The moved-cube corrector has the zero trace on the truncated window.
The datum-split competitor package.
Every clause of the second disjunct of
excessDecay_stepFour_slot_allCentres_datumSplit_errorWeighted,
produced at a boundary centre from the slot's OWN moved-cube replacement pair.
The only input beyond the slot's binders is hgradh, the classical C¹ half
of the printed datum hypothesis h ∈ C^{1,1/2}(□_m).
2. The slot with the competitor disjunction discharged #
The Step-4 decay at every centre, the disjunction discharged.
The slot with its competitor disjunction produced rather than carried, so the
boundary branch is available at a centre where the interior cube gate holds at
no scale. The binder block is the slot's own, plus the classical C¹ half
hgradh of the printed datum hypothesis h ∈ C^{1,1/2}(□_m); see the module
docstring.