Foundation Pair Kernel Relation Locality Band Weight Inhabits Finite Range Expor

Bounded recognition

In the Recognition Science framework, a ledger (a discrete record of events) carries weights between its entries. The declaration bandWeight_inhabits_finiteRange_export_v1 establishes a conditional fact: if a recognition relation is metrically bounded at radius R, and every nonzero weight is supported on that relation, then the weight graph is FiniteRange R. In plain terms, if recognition only connects sites within a fixed distance, and all nonzero weights respect that distance, then no weight reaches beyond that distance.

The theorem is proved in the machine-checked library of formal theorems. It is a real implication, not a renaming. The proof is short: take any pair of sites with distance greater than R. Since the weight is nonzero, the recognition relation must hold. But the relation is bounded, so the distance must be at most R. Contradiction. The declaration also provides a concrete witness: the existing band graph, where weights live on the unit ball of the index metric, satisfies the conditions and therefore inhabits the export.

The theorem does not claim that recognition is actually local. An unconstrained all-true relation, where every site relates to every other, supports the mean-field weight graph and therefore does not force FiniteRange. The naive route from any RecognitionStructure to L0 is closed negative. The open obligation is named: force a production recognition carrier to satisfy BoundedRecognitionRelation from Recognition dynamics. Definitions and equalities do not discharge that obligation.

What this means for the framework: the surviving route to L0 provenance is spatial-relation support plus metric boundedness. The all-true relation route is dead. The theorem does not license the claim that FiniteRange is forced by RS, nor any identification of Green coefficients, source normalization, atomic length or energy, or protein response laws.

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

The theorem does not prove that recognition is actually local. The theorem does not force FiniteRange from any RecognitionStructure. The theorem does not identify Green coefficients, source normalization, atomic length or energy, or protein response laws.

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: