Foundation Pair Kernel Relation Locality Band Weight Supported On Band Relation

The band weight's locality

In the Recognition Science framework, a ledger (a discrete record of events) carries weights between its entries. The declaration bandWeight_supported_on_bandRelation states a simple fact about one particular way of assigning those weights, the band weight. It says that whenever the band weight between two entries is nonzero, those two entries are close: their index distance is at most 1. In other words, the band weight never reaches across a gap; it only connects neighboring sites.

This is a theorem, proved in the framework's machine-checked library of formal theorems. It is not an assumption or a definition. The proof is direct: if the distance were greater than 1, the band weight would be zero by construction, so a nonzero weight forces the distance to be small. The theorem is a bridge between two concepts: the band weight's own definition and the more general notion of a relation that supports a weight. It shows that the band weight is supported on the band relation, which is exactly the relation that pairs sites within distance 1.

The significance is that this support property combines with another theorem, finiteRange_export_v1, to yield a conclusion: the band weight graph has finite range. That means there is a fixed radius (here, 1) such that no nonzero weight connects sites farther apart than that radius. This is a locality property: influence does not propagate arbitrarily far in one step. It is a concrete, checkable instance of a more general principle: if a recognition relation is metrically bounded and supports all nonzero weights, then the weight graph is finite range.

What the theorem does not claim is broader. It does not say that the band weight is the only weight with this property, nor that any recognition structure forces finite range. In fact, the framework explicitly proves the opposite for an unconstrained relation: if the relation relates every pair of sites, then the mean-field weight is supported on it, yet that weight graph is not finite range. So the band weight's locality is a property of this particular chosen weight, not a consequence of the framework's general axioms. It is a model shadow, a hand-selected example that inhabits the export, not a derivation of the production relation.

The open question the framework names is whether a production recognition relation can be forced, from more primitive dynamics, to be bounded in this way. The band weight shows the destination is reachable; it does not show the road is forced. That forcing remains an open obligation, stated explicitly as BoundedRecognitionCouplingObligation.

theorem bandWeight_supported_on_bandRelation (n : ℕ) :
    RelationSupportsWeight (bandRelation n) (bandWeight n) := by
  intro i j hne
  simp only [bandWeight] at hne
  by_cases hle : cellDist i j ≤ 1
  · exact hle
  · simp [hle] at hne

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 _)⟩

What this page does not claim

The theorem does not claim that FiniteRange is forced by Recognition Science; it remains a hypothesis. The theorem does not claim that the band weight is the only weight supported on a bounded relation. The theorem does not claim that the band relation itself is derived from more primitive dynamics; it is a chosen model.

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: