cellDist_comm
plain-language theorem explainer
Index distance on a finite carrier is symmetric: the cell separation between sites i and j equals that between j and i. Anyone building or citing the L0 finite-range weight hypothesis needs this elementary fact for symmetric kernels. The proof is a one-line unfold of the distance definition plus Mathlib's natural-number distance commutativity.
Claim. For every $n\in\mathbb{N}$ and indices $i,j\in\{0,\ldots,n-1\}$, the index-cell distance satisfies $\mathrm{dist}(i,j)=\mathrm{dist}(j,i)$, where distance is $|i-j|$ on the underlying naturals.
background
This module formalizes Door 2 / L0: the finite-range (locality) hypothesis on ledger pair weights. Even after shift-invariant (difference-only) costs are forced, a screened mean-field kernel can remain all-to-all coupled; excluding that route requires weights to vanish beyond a fixed index range.
The carrier is abstractly Fin n. Cell distance is the placeholder geometry $|i-j|$ via Nat.dist on the underlying values; it only needs to separate far-apart indices so a range cutoff is well-defined. The module's named hypothesis FiniteRange G R says the weight between sites more than R cells apart is zero.
Upstream, the distance definition is local to this file. Mathlib supplies commutativity of natural distance. The broader RS setting (tick, eight-tick octave, cost classes) is ambient but not used in this lemma.
proof idea
Term/tactic one-liner. Unfold the definition of cell distance (absolute difference of the Fin values as naturals), then apply Mathlib's Nat.dist_comm, which states $|a-b|=|b-a|$ on $\mathbb{N}$. No case splits or induction.
why it matters
Symmetric distance is required so nearest-neighbor band weights can be declared as admissible WeightedLedgerGraph objects (nonnegative and symmetric). Downstream, bandWeight uses this commutativity in its symmetry proof: coupling 1 when cell distance is at most 1, else 0.
That band graph is the non-vacuity witness for L0: it satisfies FiniteRange 1 and is admissible, while the mean-field counterexample that survives L1 fails finite range at every fixed radius on large carriers. The lemma is bookkeeping, but without it the discriminating locality hypothesis cannot even be stated on a symmetric weight graph.
It does not close the open provenance of L0 itself (expected via atomic-tick nearest-neighbor adjacency); it only makes the geometry of the cutoff well-behaved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.