finiteRange_is_discriminating
plain-language theorem explainer
The finite-range locality hypothesis is both non-vacuous and load-bearing: a nearest-neighbor band graph satisfies it at radius 1, while the all-to-all mean-field graph that carries the screening counterexample violates it at every fixed radius once the carrier is large enough. Anyone citing L0 as a discriminating postulate would use this bundle. The proof is a one-line pairing of the two component theorems.
Claim. For every carrier size $n$, the nearest-neighbor band weight graph satisfies the finite-range condition at radius $1$; and for every radius $R$ and every $n \ge R+2$, the uniform all-to-all mean-field weight graph fails the finite-range condition at radius $R$.
background
Door 2 / L0 isolates a locality postulate on the ledger weight graph that L1 and the shift-invariance bridge do not supply. Even a theorem-grade difference-only cost admits a screened, all-to-all mean-field kernel; excluding that route needs weights to vanish beyond a fixed range.
FiniteRange G R asserts that the weight between sites more than $R$ index-cells apart is zero. The band weight graph couples only nearest neighbors (weight 1 at cell distance $\le 1$, else 0). The mean-field weight graph couples every pair with weight 1, including maximally separated sites; it is the carrier of the built screening honest-negative that survives L1.
Upstream, the band graph is proved finite-range at radius 1, and the mean-field graph is proved not finite-range at any fixed $R$ once $n \ge R+2$ (sites $0$ and $R+1$ remain coupled).
proof idea
One-line term proof: pair the two component theorems into a conjunction. The left conjunct is the universal statement that every band graph is finite-range at radius 1; the right is the universal statement that mean-field fails finite-range at every fixed radius on large enough carriers. No new reasoning is introduced.
why it matters
This is the L0 status bundle: it packages non-vacuity and teeth so the finite-range hypothesis is neither empty nor trivially true. The module doc is explicit that L0 is genuinely un-formalized elsewhere on the Lean surface (a different locality in LocalityFromLedger concerns scale-level adjacency, not a pair-kernel range cutoff). Without this discrimination, the mean-field screening counterexample that survives shift-invariance would remain admissible.
The declaration does not close provenance: the doc-comment keeps L0 at HYPOTHESIS tier, with expected closure via atomic-tick / recognition adjacency being nearest-neighbor. It also does not prove "finite range $\Rightarrow$ no screening"; that dispersion step is measured in the L2 harness. No downstream consumers are wired yet; the bundle exists so later forcing or bridge work can cite a single discriminating package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.