Foundation Pair Kernel Relation Locality Local Recognition Structure Supports Fi

The locality guarantee

In the Recognition Science framework, a ledger (a discrete record of events) carries weights between its sites, and a recognition relation decides which pairs of sites can interact. The declaration localRecognitionStructure_supports_finiteRange proves a clean implication: if the recognition relation only connects sites within a fixed index distance, and if every nonzero weight sits on such a relation, then the weight graph has finite range at that same distance. Finite range here means no weight leaps across a gap larger than the allowed radius. The proof is a short argument by contradiction: a weight beyond the radius would violate the relation's boundedness, so it cannot exist.

The theorem rests on two definitions. BoundedRecognitionRelation says the relation only relates sites within a fixed index radius. RelationSupportsWeight says every nonzero pair weight implies the relation holds for that pair. The export theorem finiteRange_export_v1 packages the same implication as a reusable interface. A concrete witness exists: the band geometry, which connects sites within distance one, satisfies the export and gives a finite-range weight graph.

The framework also proves a negative result that sharpens the boundary. An unconstrained relation, one that connects every pair of sites, supports the mean-field weight graph and does not force finite range. The naive route from any recognition structure to finite range is closed. The locality guarantee therefore requires the boundedness premise; it is not automatic.

In Recognition Science, this theorem is a step toward deriving the locality of physical interactions from recognition dynamics. But the theorem does not claim that recognition dynamics actually force the boundedness condition. That forcing remains an open obligation, named BoundedRecognitionCouplingObligation in the library. The theorem supplies the conditional: if locality holds, then finite range follows. The task of deriving that if from more primitive principles is not discharged here.

/-- If nonzero weights live inside the local recognition structure, L0 follows
from the export. -/
theorem localRecognitionStructure_supports_finiteRange
    {n radius : ℕ} {G : WeightedLedgerGraph n}
    (hS : RelationSupportsWeight (localRecognitionStructure n radius).R G) :
    FiniteRange G radius :=
  finiteRange_export_v1 (localRecognitionStructure_bounded n radius) 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 boundedness condition is derived from deeper dynamics. Any RecognitionStructure implies finite range.

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: