bandWeight_finiteRange
plain-language theorem explainer
The nearest-neighbor band weight graph on any finite carrier satisfies the finite-range locality hypothesis at radius one: couplings vanish beyond one cell. Anyone citing L0 non-vacuity or the discriminating status of that hypothesis needs this witness. The proof unfolds the band weight definition against the distance hypothesis and reads off the zero branch.
Claim. For every carrier size $n$, the nearest-neighbor band weight graph (weight $1$ when cell distance is at most $1$, else $0$) satisfies the finite-range locality hypothesis at radius $1$: whenever two sites are more than one cell apart, their pair weight is zero.
background
This module is Door 2 / L0 on the pair-kernel provenance lane: a named locality hypothesis on ledger weight graphs. On-site exclusion and the shift-invariance bridge still leave room for a screened, Yukawa-like mean-field kernel that is difference-only and shift-invariant yet all-to-all coupled. Killing that route needs a separate postulate that weights vanish beyond a fixed range.
Finite-range at radius $R$ means: for all sites $i,j$, if cell distance exceeds $R$ then the graph weight is zero. The band weight graph is the admissible nearest-neighbor graph with weight $1$ on pairs at distance at most $1$ and $0$ otherwise. The module's mean-field carrier violates finite range at every fixed $R$ once the carrier is large enough; this theorem is the matching positive witness that the hypothesis is inhabited.
proof idea
Short tactic proof. Introduce sites $i,j$ and the hypothesis that cell distance exceeds $1$. Unfold the band weight: it is the conditional "if cell distance $\le 1$ then $1$ else $0$". The distance hypothesis is exactly the negation of $\mathrm{cellDist}\le 1$, so if_neg (via not_le.mpr) selects the else branch and yields weight $0$, which is the finite-range obligation at radius $1$.
why it matters
Feeds the L0 status bundle finiteRange_is_discriminating: finite range is (a) satisfied by an admissible non-trivial graph (the band graph at radius $1$) and (b) violated by the mean-field screening carrier at every fixed radius for large enough carriers. A hypothesis with both teeth is neither vacuous nor automatic.
Module scope is honest: L0 remains HYPOTHESIS-tier; its RS provenance (a forced range cutoff from atomic-tick / recognition adjacency) is still OPEN. This declaration only closes non-vacuity. It does not prove "finite range $\Rightarrow$ no screening"; that dispersion/Fourier step is measured in the L2 harness, not re-proved here. Together with the mean-field negative, it keeps screened all-to-all kernels out of the admissible local cost class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.