Foundation Pair Kernel Relation Locality

The locality export

In Recognition Science, a ledger is a discrete record of events, and a recognition relation is a rule saying which pairs of sites can interact. The module PairKernelRelationLocality asks a precise question: if that rule only connects sites within a fixed index radius, does the weight graph, the collection of nonzero interaction strengths, have to be finite-range, meaning no weight reaches beyond that radius?

The answer is yes, and it is proved as a theorem. The formal statement, finiteRange_export_v1, says that if a recognition relation is metrically bounded at radius R, and every nonzero weight is supported on that relation, then the weight graph is finite-range at R. This is a genuine implication, not a renaming of the conclusion. The proof is short: a weight at distance greater than R would violate the relation's boundedness, so no such weight can exist.

The module also closes a tempting but false route. An unconstrained relation, one that relates every site to every other, supports the mean-field weight graph and therefore does not force finite-range behavior. The theorem unconstrainedRelation_does_not_force_finiteRange makes this obstruction explicit. The naive claim that any recognition structure implies locality is closed negative.

As a positive shadow, the module exhibits a hand-selected band geometry: a relation that connects sites within unit distance supports the existing band weight graph, and this inhabits the export. This shows the implication is not vacuous, though it does not force the production relation.

In Recognition Science, the framework models this as the surviving route to L0 provenance, the property that interaction weights are spatially local. The open obligation is now exact: force a production recognition relation to be bounded from Recognition dynamics themselves. That forcing remains a hypothesis, not a theorem.

theorem finiteRange_export_v1
    {n radius : ℕ} {R : Fin n → Fin n → Prop} {G : WeightedLedgerGraph n}
    (hB : BoundedRecognitionRelation R radius)
    (hS : RelationSupportsWeight R G) :
    FiniteRange G radius :=
  boundedRecognitionRelation_supports_finiteRange hB hS

/-- **CLOSED NEGATIVE.** An unconstrained recognition relation supports the
screening mean-field graph, so "any RecognitionStructure ⇒ FiniteRange" is false. -/
theorem unconstrainedRelation_does_not_force_finiteRange (radius : ℕ) :
    ∃ n : ℕ,
      (∀ i j : Fin n, unconstrainedRelation n i j) ∧
        RelationSupportsWeight (unconstrainedRelation n) (meanFieldWeight n) ∧
          ¬ FiniteRange (meanFieldWeight n) radius := by
  refine ⟨radius + 2, fun _ _ => trivial,
    meanFieldWeight_supported_on_unconstrained (radius + 2),
    meanFieldWeight_not_finiteRange radius (radius + 2) (le_refl _)⟩

/-- MODEL shadow integration: the hand-selected band carrier inhabits
`finiteRange_export_v1`. This does not force the production relation. -/
theorem bandWeight_inhabits_finiteRange_export_v1 (n : ℕ) :
    BoundedRecognitionRelation (bandRelation n) 1 ∧
      RelationSupportsWeight (bandRelation n) (bandWeight n) ∧
        FiniteRange (bandWeight n) 1 :=
  ⟨bandRelation_bounded n,
    bandWeight_supported_on_bandRelation n,
    finiteRange_export_v1 (bandRelation_bounded n)
      (bandWeight_supported_on_bandRelation n)⟩

What this page does not claim

FiniteRange is forced by Recognition Science from first principles. The production recognition relation is bounded. The band geometry is the unique or actual recognition carrier.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PairKernelRelationLocality.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: