bandWeight
plain-language theorem explainer
Nearest-neighbor band weight on an n-site ledger carrier: edge weight 1 when index distance is at most 1, else 0. It is an admissible WeightedLedgerGraph (nonnegative, symmetric). Anyone citing FiniteRange non-vacuity or the L0 discriminating bundle uses this witness. Structure fields are discharged by case split on the threshold and symmetry of cell distance.
Claim. For each $n \in \mathbb{N}$, the band weight is the weighted ledger graph on the $n$-site carrier whose weight between sites $i$ and $j$ is $1$ if the index distance $|i-j| \le 1$ and $0$ otherwise. The weight is nonnegative and symmetric in its two arguments.
background
Door 2 / L0 isolates a finite-range (locality) hypothesis on pair weights of a ledger graph. Shift-invariance alone does not kill screened all-to-all kernels: the mean-field counterexample is difference-only yet couples every pair, and that route needs a separate cutoff. FiniteRange G R asserts that the weight vanishes whenever index distance exceeds fixed radius $R$.
Index geometry here is placeholder only: cellDist i j is Nat.dist of the Fin n values, so far-apart indices are separated. The module does not derive range from first principles; it names the postulate, shows it rejects mean-field, and shows it is inhabited.
A weighted ledger graph packages a real weight with nonnegativity and symmetry. The band construction is the canonical nearest-neighbor instance used as the positive witness.
proof idea
Definitional construction: set weight i j to the indicator of cellDist i j ≤ 1. Nonnegativity is a one-line case split on that conditional, each branch closed by norm_num. Symmetry rewrites the left-hand threshold via cellDist_comm, so the two conditionals agree. No external cost lemmas are needed; only the local distance API.
why it matters
This is the concrete admissible graph that makes L0 non-empty. Downstream, bandWeight_finiteRange proves it satisfies FiniteRange at radius 1, and bandWeight_adjacent_coupled shows nearest neighbors really couple (weight 1 on sites 0 and 1), so the witness is not the trivial diagonal. Those two facts feed finiteRange_is_discriminating, the L0 status bundle: FiniteRange is satisfiable by a non-trivial admissible graph and violated by mean-field at every fixed radius on large carriers.
In the pair-kernel provenance lane this closes the "hypothesis empty?" objection after on-site exclusion and the shift-invariance bridge. It does not force the cutoff from T0–T8 or the RCL; RS provenance of a forced range remains open. Dispersion "L0 ⇒ no screening" stays measured in the L2 harness, not proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.