BoundaryPrefactor #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The boundary Caccioppoli prefactor at the slot n+3, on the covering cube #
The boundary lane's Caccioppoli inequality runs on the covering cube c + □_{n+2}, c = wellPlacedCentre x m (n+2), and its right-hand side carries two
coarse-grained factors: CoarseGraining's caccioppoliWith a s_c t and the
lower constant λ_t(Q; a). BoundaryCoveringSlot capped the covering
cube's q = 2 ratio pair at the coarse-graining slot s/6; this module
reads the caps at the pair of indices the boundary Caccioppoli actually
consumes and turns them into a d-only bound on the prefactor.
The parameter pair #
The proved interior chain runs the Caccioppoli at (s_c, t) = (1/4, s/4).
That pair is not available off-grid: its lower ingredient needs the q = 2
ratio at (s/4)/2 = s/8, and the off-grid transport of
BoundaryCoveringSlot (ae_coveringCubeError_le_representative) requires
an index strictly above the good-event slot s/8. The boundary lane
therefore runs at
(s_c, t) = (1/2, s/3) ,
whose two ratio indices are 1/4 and s/6, both strictly above s/8 for
every s ∈ (0,1], and which satisfies CoarseGraining's own range conditions 0 < s_c < 1, 0 < t < 1/2, s_c + t < 1. The pair costs no s-power: the
prefactor's middle factor is s_c^{-2s_c/σ} at the first parameter s_c = 1/2, a pure number.
References #
- ABK26,
l.coarse.grained.Caccioppoli.RHS; the boundary application.
1. The off-grid constant at the upper index #
The off-grid stability constant at the pair (1/4, s/8).
36 d (1/4) / ((1/4 − s/8)(1 − s/4)) ≤ 96 d for every s ∈ (0,1]; the
extremal configuration is s = 1, where the denominator is 3/32. (The
proved slot bound is offGridStabilityConst_slot_le at (s/6, s/8); this is
its sibling at the upper index, and 96 d ≤ 192 d, so both are absorbed by the
same κ.)
2. The coarse-grained caps at the boundary pair #
Covering-cube caps under explicit half-open parent containment.
The covering cube's q = 1 ingredients at the boundary Caccioppoli
pair.
On the frozen general clause's own good event 𝒢(n+3, z; s/8, 1/2), the
coarse-grained ellipticity data of the (n+3) re-based family on the covering
cube — the upper constant at 1/2, the lower constant at s/3, and their
contrast — are all controlled by one d-only constant K against σ_{n+3}.
3. The prefactor at the boundary pair #
The prefactor at (s_c, t) = (1/2, s/3) is a constant.
For every s ∈ (0,1], every C > 0 and every cap Θ ≤ Θ₀,
(C/σ)^{2+4·(1/2)/σ} · (1/2)^{-2·(1/2)/σ} · Θ^{(1−s/3)/σ}
≤ (6C)^{14} · 64 · Θ₀^6 , σ = 1 − 1/2 − s/3 ∈ [1/6, 1/2) .
Every step is a rational comparison of rpow exponents; no transcendental
estimate and no s-power is used.
4. The coarse-grained prefactor on the covering cube #
The boundary prefactor under explicit half-open parent containment.
The boundary Caccioppoli's two coarse-grained factors, capped.
On the frozen good event, the boundary Caccioppoli's prefactor at the pair
(1/2, s/3) and its lower constant λ_{s/3} — both read on the covering cube
at the (n+3) re-based family, with no Λ/λ converted by invariance — are
controlled by one constant depending on d and CoarseGraining's own
Caccioppoli constant, times σ_{n+3} for the lower constant. No s-power
is spent.