FiniteRange
plain-language theorem explainer
Finite-range locality on a weighted ledger graph: edge weights vanish once index distance exceeds a fixed radius R. Pair-kernel / Door-2 workers cite it as the named L0 hypothesis that shift-invariance and the ratio bridge do not supply. The body is a pure universal Prop over site pairs, measured by cell distance; no derivation is claimed.
Claim. A weighted ledger graph $G$ on $n$ sites is finite-range at radius $R$ when, for all sites $i,j$, if the index distance satisfies $\mathrm{dist}(i,j) > R$, then the coupling weight $G_{ij}$ is zero.
background
Door 2 / L0 sits in the pair-kernel provenance lane. On-site mass exclusion was already conditional on shift-invariance (difference-only cost), and the ratio bridge made shift-invariance model-forced. That still leaves screened, Yukawa-like kernels: the mean-field all-to-all carrier is difference-only and shift-invariant yet couples every pair, producing a mass gap away from $k=0$. Killing that route needs a separate locality cut on the weights.
cellDist is the placeholder geometry: index distance $|i-j|$ on the Fin n carrier. It only has to separate far-apart indices; a range cutoff needs nothing more. The module scan found no prior range principle on WeightedLedgerGraph in the Lean surface (LocalityFromLedger is a different, scale-level adjacency). So L0 is named explicitly rather than smuggled in via lattice adjacency the L2 harness happened to use.
proof idea
Pure definition, not a proved theorem. The predicate is the universal statement: for every pair of sites $i,j$ in the finite carrier, if $R < \mathrm{cellDist}(i,j)$ then $G.weight,i,j = 0$. No tactics, no lemmas; just the Prop that later theorems inhabit or refute.
why it matters
L0 is the load-bearing locality cut that L1 cannot supply. Downstream, bandWeight_finiteRange shows non-vacuity: the nearest-neighbor band graph is an admissible cost inside FiniteRange at radius 1. The teeth theorems meanFieldWeight_not_finiteRange and meanFieldLedgerCost_not_finiteRange show the built screening honest-negative violates the predicate at every fixed $R$ once the carrier is large enough. Those two directions package as finiteRange_is_discriminating: satisfiable and rejecting, so the hypothesis does real work.
Framework role: without a range cut, shift-invariant all-to-all coupling survives and screens. Provenance of the cutoff itself remains OPEN (expected closure via atomic-tick / recognition adjacency being nearest-neighbor). This module does not prove "L0 implies no screening"; that dispersion step is measured in the L2 harness, not re-proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.