cellDist
plain-language theorem explainer
Index distance on a finite carrier: the absolute difference of two site labels in Fin n. Anyone stating a range cutoff on pair weights cites it as the geometry that separates near from far. The definition is a one-line wrapper of Nat.dist on the underlying naturals.
Claim. For a finite carrier of size $n$ and sites $i,j\in\{0,\ldots,n-1\}$, the cell distance is $|i-j|$.
background
Door 2 / L0 formalizes a finite-range (locality) hypothesis on ledger weight graphs. Pair-kernel work already forces shift-invariant, difference-only costs, but that alone does not kill all-to-all screened (mean-field) kernels. A separate postulate is needed: weights vanish beyond a fixed range.
The carrier is an abstract Fin n of sites. Cell distance is the placeholder metric on that carrier: ordinary absolute difference of indices. It is not a physical lattice metric; it only needs to mark which pairs are farther than a cutoff radius $R$.
That distance is the primitive used by the named hypothesis FiniteRange and by the nearest-neighbor band graph that witnesses non-vacuity of the hypothesis.
proof idea
One-line definition: unwrap the Fin indices to naturals and apply Mathlib's Nat.dist (absolute difference). No proof obligations.
why it matters
Cell distance is the geometry under L0. FiniteRange is literally "weight vanishes when cellDist exceeds R". Downstream, bandWeight sets coupling 1 exactly when cellDist ≤ 1, and bandWeight_adjacent_coupled checks that adjacent sites really couple. The teeth theorem meanFieldWeight_not_finiteRange builds a far pair via cellDist to show the all-to-all mean-field graph fails every fixed radius once the carrier is large enough.
In the Recognition stack this is scaffolding for the locality postulate that L1 and the ratio bridge do not supply. Provenance of L0 itself remains open (expected from atomic-tick / recognition adjacency being nearest-neighbor). The module does not yet prove "finite range ⇒ no screening"; that is the L2 dispersion step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.