IndisputableMonolith.Foundation.PairKernelLocality
Defines locality for pair kernels on a finite carrier: index distance, the FiniteRange predicate, and a discriminating band weight that couples only adjacent sites. Mean-field weights fail finite range; the band weight satisfies it. Downstream discrete Gauss work imports this as the locality hypothesis after onsite exclusion. Arguments are mostly direct unfoldings and Nat.dist arithmetic.
claimOn a carrier $\mathrm{Fin}\, n$, the cell distance is $d(i,j)=|i-j|$. A pair weight $W$ has finite range if there exists $R$ such that $W(i,j)=0$ whenever $d(i,j)>R$. Mean-field (all-to-all) weights are not finite-range for $n$ large enough; a nearest-neighbor band weight is finite-range with $R=1$ and couples adjacent sites. Finite range is a discriminating locality test against nonlocal kernels.
background
Door 2 of the pair-kernel provenance lane asks which interaction structures are compatible with recognition cost after onsite terms are excluded. The upstream module closes shift-invariance for pure difference costs and frames the L1-hard onsite-exclusion step; this module supplies the next geometric filter: locality of the pair kernel.
The carrier is abstract $\mathrm{Fin}, n$ with placeholder geometry $\mathrm{cellDist}(i,j)=|i-j|$ (via $\mathrm{Nat.dist}$). Only separation of far indices matters for a range cutoff. $\mathrm{FiniteRange}$ asserts existence of a radius $R$ beyond which the pair weight vanishes. Mean-field / all-to-all ledger weights are the nonlocal foil; a band (nearest-neighbor) weight is the local prototype.
The setting is deliberately pre-metric: no continuum limit, no physical lattice embedding yet. The point is a Lean-checkable dichotomy between kernels that die at finite hop distance and those that do not.
proof idea
Definition-heavy module with short lemmas. $\mathrm{cellDist}$ is $\mathrm{Nat.dist}$ on indices; commutativity is immediate from symmetry of absolute difference. $\mathrm{FiniteRange}$ is an existential predicate on pair weights. Non-locality of mean-field weights is by exhibiting pairs with arbitrarily large index separation still carrying nonzero weight when $n$ exceeds any candidate $R$. Band weight is defined to vanish off adjacency, so $R=1$ witnesses finite range; a separate lemma records that adjacent sites remain coupled. The discriminating lemma packages the contrast: finite range rejects mean-field and accepts the band kernel.
why it matters in Recognition Science
Feeds $\mathrm{PairKernelDiscreteGauss}$, which treats $\mathrm{FiniteRange}$ as the locality hypothesis after the shift-invariant pair-cost carrier. Downstream doc-comment: after pair-cost and locality, the next vertebra is the discrete Gauss / continuity law (divergence of recognition current equals local sigma-imbalance; lattice integral gives zero net source).
In the provenance lane this is the geometric half of Door 2: onsite exclusion removes local mass terms; finite range removes infinite-range mean-field coupling. Together they pin the admissible kernel shape before flux identities. Relates to the broader forcing program only indirectly (structure of the cost, not yet T5–T8 constants). Closes a negative atomic-tick provenance note on nonlocal kernels while leaving $\mathrm{FiniteRange}$ itself as a named hypothesis for later discharge or specialization.
scope and limits
- Does not prove FiniteRange from first principles; it is a hypothesis interface for downstream Gauss work.
- Does not embed Fin n into physical R^3 or the eight-tick octave geometry.
- Does not derive the band weight from the J-cost or RCL; band weight is a test kernel.
- Does not address continuum limits, renormalization, or Hessian dispersion numerics.
- Does not claim mean-field is impossible in nature; only that it fails the finite-range predicate.