SlotTransportChildCube #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Transporting the good-event caps from the parent cube to sub-cubes #
The printed consumers read them at sub-cubes of the parent and at the
larger indices s/6 and s/4:
e.good.set.giveth.v2atx+□_{n+1}, indicess/4(q = 1) ands/6(q = 2);e.bound.Lambdas.by.Es.v2atx+□_{n+1}, indexs/4,q = 2— the input of the coarse-grained Caccioppoli stepe.energy.bound.interior, whose Caccioppoli pair is(x+□_n) ⊂ (x+□_{n+1}), so the outer cube of that pair is where the ellipticity ratios are needed.
This module performs that transport for triadic sub-cubes of the parent, at
the field and comparator of the parent (which is exactly how the manuscript
writes it: 𝓔_{t,∞,q}(y+□_{n+1}; ã_{L,n+2}, σ_{n+2}), the parent's
flux-corrected field on the smaller cube).
What is transported, and what is NOT #
Transported (proved below, unconditionally):
- the index change
s/8 → ufor everyu ≥ s/8, at no cost —𝓔is antitone in its index (StabilityIndexCube.lean); - the scale-exponent change
q = 2 → q = 1, at no cost, via the manuscript's owne.compareEqs(StabilityExponentComparison.lean): it converts𝓔_{s/4,∞,1}into𝓔_{s/8,∞,2}, i.e. straight onto the annular anchor's own index; - the cube change parent → triadic descendant at depth
h, at cost3^{(s/8)·h}(≤ 3^{1/8} < 1.15for a one-scale descent ands ≤ 1).
In CoarseGraining's carrier the shells of an off-grid cube are maxima over the
translated grid, which is disjoint from the parent's grid, so no inclusion or
monotonicity argument reaches them; the printed route is l.lambdas.stability,
whose proof is a greedy Whitney-type decomposition of the off-grid cube by
parent-grid subcubes at all deeper scales, plus subadditivity of σ_*^{-1} and
a packing count.
Consequently the geometry lemma proved here — the child inclusion that the manuscript itself silently uses — is recorded as a verified input to that missing lemma, not as a substitute for it.
Main definitions #
fluxCorrectedErrorOn—𝓔_{s,∞,2}(Q; ã_{L,m}, σ_m)for an arbitrary triadic cubeQ, at the flux-corrected field and comparator of□_m. The manuscript's shorthand; atQ = □_mit isSupport.fluxCorrectedError.fluxCorrectedErrorOnOne— itsq = 1sibling, the quantity the coarse-graining displaye.homogenization.L2.interiorcarries.
Main results #
image_add_openCubeSet_succ_subset— the geometry the manuscript uses without comment: the anchor's binder(x+□_n) ⊆ (z+□_{n+1}) ∩ □_mimplies(x+□_{n+1}) ⊆ (z+□_{n+2}), the inclusion the proof restates.ae_errorOn_descendant_le_harmonicSlot— theq = 2cap at every triadic sub-cube and every indexu ≥ s/8.ae_errorOnOne_descendant_le_harmonicSlot— theq = 1cap at every triadic sub-cube and every indexu ≥ s/4: the first inequality ofe.good.set.giveth.v2, in the grid rendering.ae_boundLambdasByEs_descendant_harmonicSlot—e.bound.Lambdas.by.Es.v2at every triadic sub-cube and every indexu ≥ s/8, in the grid rendering.
Deviations from print, recorded #
- Grid, not continuum. All three cap statements quantify over
descendantsAtScale (originCube d (n+2)) k, never over translates. Nothing below is presented ase.mathcalE.stability.appliedor asl.lambdas.stability. - The printed intermediate rung is skipped. The printed chain goes
𝓔_{s/4,∞,1} ≤ C 𝓔_{s/6,∞,2} ≤ 𝓔_{s/8,∞,2} ≤ C. The route here is𝓔_{s/4,∞,1} ≤ 𝓔_{s/8,∞,2}(same cube) ≤ 3^{(s/8)h} 𝓔_{s/8,∞,2}(parent) ≤ C/2: the same endpoint, one rung fewer, and with explicit constants. The printed first inequality itself (at the indexs/6) is not proved; seeStabilityExponentComparison.lean.
References #
- ABK26,
e.good.set.giveth.v2,e.bound.Lambdas.by.Es.v2. - ABK26,
e.mathcalE.stability.applied. - ABK26,
e.energy.bound.interior. - ABK26,
l.lambdas.stability;e.compareEqs.
1. The geometry the manuscript uses without comment #
2. The parent's functionals read at a sub-cube #
𝓔_{s,∞,2}(Q; a_L − (κ_L−κ_m)_{□_m}, σ_m): the parent's flux-corrected
field and comparator, evaluated on an arbitrary triadic cube Q.
This is the manuscript's own shorthand — the display carries
𝓔_{s/6,∞,2}(y+□_{n+1}; ã_{L,n+2}, σ_{n+2}), i.e. the field and comparator of
the parent cube z+□_{n+2} on the smaller cube. Translated centres are
realized, as everywhere in Section 4, by translating the sample (resolution
A4).
Equations
- One or more equations did not get rendered due to their size.
Instances For
max{σ_m⁻¹Λ_{s,2}(Q), σ_mλ_{s,2}⁻¹(Q)} at the parent's field and comparator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At the cube that carries the flux correction, the sub-cube functional is the
proved literal error of ErrorAtoms.
3. The q = 2 cap at every triadic sub-cube #
The caps step transported to triadic sub-cubes and to every larger index.
On the harmonic statement's good event 𝒢(n+2, z; s/8, 1/2), for every
L ≥ n+2, every triadic descendant Q of □_{n+2} at scale k, and every
index u ≥ s/8,
𝓔_{u,∞,2}(Q; ã_{L,n+2}, σ_{n+2}) ≤ 3^{(s/8)·(n+2−k)} · C/2 .
The index change is free and the cube change costs the explicit factor; the
right-hand side is a constant, which is what the downstream Caccioppoli and
coarse-graining steps consume. At k = n+1 and u = s/6 this is the middle
inequality of e.good.set.giveth.v2 in its grid rendering (deviation 1).
4. The q = 1 cap: the first inequality of e.good.set.giveth.v2 #
5. e.bound.Lambdas.by.Es.v2 at every triadic sub-cube #
e.bound.Lambdas.by.Es.v2 transported to triadic sub-cubes.
On the harmonic statement's good event, for every L ≥ n+2, every triadic
descendant Q of □_{n+2} at scale k and every index u ≥ s/8,
max{ σ_{n+2}⁻¹Λ_{u,2}(Q; ã_{L,n+2}) , σ_{n+2}λ_{u,2}⁻¹(Q; ã_{L,n+2}) }
≤ 2d ( (3^{(s/8)(n+2−k)} · C/2)² + 1 ) .
This is the input the coarse-grained Caccioppoli step e.energy.bound.interior
consumes, at the outer cube of its Caccioppoli pair — provided that outer
cube is a triadic descendant of the parent.
e.bound.Lambdas.by.Es.v2 at the parent cube, for every index
u ≥ s/8.
max{ σ_{n+2}⁻¹Λ_{u,2}(z+□_{n+2}; ã) , σ_{n+2}λ_{u,2}⁻¹(z+□_{n+2}; ã) } · 1_𝒢
≤ 2d((C/2)² + 1) .