meanFieldWeight_not_finiteRange
plain-language theorem explainer
On a carrier of size at least R+2, the uniform all-to-all mean-field weight graph fails finite-range locality at every fixed radius R: sites distance R+1 apart still carry weight 1. Anyone citing L0 as the discriminating locality hypothesis against the screening counterexample needs this tooth. The proof is a short contradiction: FiniteRange forces that pair-weight to vanish, but mean-field sets it to one.
Claim. For natural numbers $R$ and $n$ with $R+2 \le n$, the mean-field weight graph on $n$ sites (every pair coupled with weight $1$) is not finite-range at radius $R$: it is not the case that every pair of sites more than $R$ index-cells apart has vanishing weight.
background
Door 2 / L0 isolates a locality hypothesis on ledger weight graphs that L1 (shift-invariance / difference-only cost) and the ratio bridge do not supply. Even a theorem-grade shift-invariant cost admits a screened mean-field counterexample: all-to-all coupling that is difference-only yet produces a mass gap away from $k=0$. Excluding that route needs weights to vanish beyond a fixed range.
FiniteRange G R asserts that whenever the index distance cellDist i j (namely $|i-j|$ on the Fin n carrier) exceeds $R$, the edge weight $G.weight,i,j$ is zero. The mean-field weight is the constant graph with every pair weight equal to $1$; it is the carrier of the built honest-negative meanFieldLedgerCost. Index distance is only a placeholder geometry: what matters is that far-apart indices are separated, which is all a range cutoff needs.
The module does not derive L0 from anything more primitive. Provenance is open, with expected closure via atomic-tick / recognition adjacency being nearest-neighbor. The job here is teeth: show the hypothesis genuinely rejects the screening carrier that survives L1.
proof idea
Assume toward contradiction that the mean-field weight on $n$ sites is finite-range at radius $R$, under $R+2\le n$. The size hypothesis gives $0<n$ and $R+1<n$, so the Fin-sites $0$ and $R+1$ are well-defined. Their cell distance is $\mathrm{Nat.dist}(0,R+1)=R+1$, hence strictly greater than $R$. Finite-range therefore forces the mean-field weight on that pair to be $0$. Unfolding the mean-field definition yields weight $1$, and $1\ne 0$ closes the contradiction. Pure arithmetic (omega) plus one simp on the weight definition; no external lemmas beyond the local cellDist / FiniteRange definitions.
why it matters
This is the load-bearing half of the L0 status bundle. Downstream, meanFieldLedgerCost_not_finiteRange is the one-line transfer to the built honest-negative cost ("L0 is exactly the hypothesis that rejects the screening carrier that survives L1"), and finiteRange_is_discriminating packages it with non-vacuity of the nearest-neighbor band graph: FiniteRange is satisfiable and violated, so neither empty nor trivial.
In the pair-kernel provenance lane, L1 closed on-site-mass exclusion under shift-invariance, but left the Yukawa-like mean-field route open. L0 is the separate postulate that cuts that route at the weight-graph level. The module still does not prove "L0 ⇒ no screening" (dispersion/Fourier remains measured in the L2 harness). RS provenance of a forced range cutoff remains OPEN; expected closure is nearest-neighbor recognition adjacency on the atomic tick, not a silent appeal to the $4^3$ lattice the harness happened to use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.