HomSpineDepthFarBandSize #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The EXACT size of the far-band half: min(j·log 3, (s·p')^{-1}) #
Why #
HomSpineCzGridDepthTest §4 records the far half of the single-depth
boundary-layer estimate as the truncated geometric sum
Σ_{i<j} 3^{-i·s·p'}, proves it ≥ j/3 on the window j·s·p' ≤ 1, and
proves it UNBOUNDED over the admissible (s, j) range. That leaves open the
size at a FIXED order — the quantity this development actually pays, since the
Step-3 pin fixes s ≍ |log γ|^{-1} and then lets j run to 10|log γ|.
This file closes the arithmetic with a two-sided bound. Writing x = s·p':
min( j/3, (2/(3 log 3))·x^{-1} ) ≤ Σ_{i<j} 3^{-x i} ≤ (1 - 3^{-x})^{-1}
(the upper bound is farBand_sum_le_geom), and the right side is itself
≤ (x log 3)^{-1}·(1-3^{-x})^{-1}(1-3^{-x}), i.e. of the same x^{-1} order —
so the far half is ≍ min(j, x^{-1}), saturating at x^{-1} once j ≥ x^{-1}.
Consequence for the surviving route (the DEPTH-level converse, the
per-cell one having been refuted in HomSpineSupFormCellRefuted): the constant
the single-depth Gagliardo input can carry is
Cg^{p'} ≍ C(d) + min(j·log 3, (s·p')^{-1}), hence at the Step-3 pin
CA ≍ |log γ|^{1/p'} — NOT γ-uniform, and the deficit is exactly the
Gagliardo-vs-Besov (Bourgain--Brezis--Mironescu) constant of the test space as
s → 0. This file proves the arithmetic; the identification with Cg is
The fullENorm_gridDualDepthTest_le_of_gagliardo slot and is NOT claimed
here.
The far half is at most the full geometric sum (1-3^{-x})^{-1}: at a
fixed order the band sum saturates, it does not grow with the depth.