meanFieldLedgerCost_not_finiteRange
plain-language theorem explainer
The mean-field ledger cost that survives on-site exclusion has a weight graph that is never finite-range: for any fixed radius R, once the carrier has at least R+2 sites, some pair beyond distance R still couples. Anyone arguing that the L0 locality hypothesis is load-bearing against screened (Yukawa-like) kernels cites this. The proof is a one-line transfer of the same fact already proved on the underlying mean-field weight graph.
Claim. For all natural numbers $R$ and $n$ with $R + 2 \le n$, the weight graph of the mean-field ledger cost on $n$ sites fails finite-range at radius $R$: there exist sites more than $R$ cells apart whose coupling weight is nonzero.
background
Door 2 / L0 isolates a locality hypothesis on ledger weight graphs that L1 (shift-invariance / difference-only cost) does not supply. Finite-range at radius $R$ means the weight between any two sites whose index-cell distance exceeds $R$ is zero: no coupling beyond a fixed range. The module states this as an explicit named hypothesis, not a derived theorem, because the Lean surface has no prior range cutoff on pair kernels.
The panel mean-field counterexample is difference-only and shift-invariant yet all-to-all coupled, so it can produce a mass gap away from $k = 0$ (screening). That carrier is the mean-field ledger cost; its weight graph couples every pair with weight 1. The sibling result already shows that weight graph fails finite-range once $n \ge R+2$. This declaration restates the same discrimination on the cost object itself (its graph field).
proof idea
One-line term proof: apply the sibling theorem that the mean-field weight graph is not finite-range at radius $R$ under the hypothesis $R+2 \le n$. The cost object's weight-graph field is definitionally that mean-field weight, so the negation transfers immediately with no extra arithmetic on cell distances.
why it matters
This is the teeth of L0 on the built honest-negative cost: finite-range rejects exactly the screening carrier that survives L1 and the pair-kernel ratio bridge. Without it, a theorem-grade shift-invariance still leaves open an all-to-all Yukawa-like kernel. The module does not prove "L0 implies no screening" (the dispersion/Fourier step is measured in the L2 harness, not re-proved here). Provenance of L0 itself remains open, with expected closure via atomic-tick nearest-neighbor recognition adjacency. No downstream consumers yet; the declaration pins the discrimination claim on the cost, not only the raw weight graph, and pairs with the non-vacuity band-weight results that show some admissible costs do satisfy finite-range.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.