Foundation Pair Kernel Relation Locality Unconstrained Recognition Relation Prov

A closed route to locality

In the Recognition Science framework, a ledger (a discrete record of events) carries weights between its sites, and a locality property called FiniteRange asks that no weight connects sites farther apart than a fixed radius. A tempting shortcut says: if every site can recognize every other site, then the weight graph must be local. The theorem unconstrained_recognition_relation_provenance_closed_negative closes that route. It establishes, in the framework's machine-checked library of formal theorems, that an all-true recognition relation does not force FiniteRange: there exists a mean-field weight graph, where every site interacts with every other, that is supported on the all-true relation yet fails to be FiniteRange at any chosen radius.

The theorem also establishes that the all-true relation is not itself bounded: it fails BoundedRecognitionRelation at that same radius. The positive statement survives intact. If a recognition relation is metrically bounded at radius R, meaning it only relates sites within that index distance, and every nonzero weight is supported on that relation, then the weight graph is FiniteRange R. This is the export interface finiteRange_export_v1, a real implication rather than a renaming. A hand-selected band geometry, where sites relate only within unit distance, inhabits this export and shows the implication is not vacuous.

The theorem's force is negative: it kills the naive route "any RecognitionStructure implies L0". Its positive content is a conditional, not a conclusion. FiniteRange itself remains a hypothesis, not a consequence of Recognition dynamics. The open obligation is now exact: force a production recognition carrier to satisfy BoundedRecognitionRelation at a fixed radius from Recognition dynamics, then transport nonzero pair weights through the support condition to FiniteRange. That obligation is named BoundedRecognitionCouplingObligation, and the theorem does not discharge it.

What the theorem changes is the map of what remains to be shown. A reader can now see that locality in this framework cannot be assumed from a recognition relation alone; it must be earned by a metric bound on the relation, which itself must be derived from more primitive dynamics. The all-true route is dead, and the surviving route is spatial support plus metric boundedness.

/-- Bundle: the surviving L0 provenance route is bounded spatial support, not
an unconstrained recognition relation. -/
theorem unconstrained_recognition_relation_provenance_closed_negative (radius : ℕ) :
    RelationSupportsWeight (unconstrainedRelation (radius + 2))
        (meanFieldWeight (radius + 2)) ∧
      ¬ FiniteRange (meanFieldWeight (radius + 2)) radius ∧
        ¬ BoundedRecognitionRelation (unconstrainedRelation (radius + 2)) radius := by
  refine ⟨meanFieldWeight_supported_on_unconstrained (radius + 2),
    meanFieldWeight_not_finiteRange radius (radius + 2) (le_refl _), ?_⟩
  intro hB
  have hi : (0 : ℕ) < radius + 2 := Nat.succ_pos _
  have hj : radius + 1 < radius + 2 := Nat.lt_succ_self _
  have hle : cellDist (⟨0, hi⟩ : Fin (radius + 2)) ⟨radius + 1, hj⟩ ≤ radius :=
    hB ⟨0, hi⟩ ⟨radius + 1, hj⟩ trivial
  have hdist :
      cellDist (⟨0, hi⟩ : Fin (radius + 2)) ⟨radius + 1, hj⟩ = radius + 1 := by
    simp only [cellDist, Nat.dist]
    omega
  omega

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

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

/-- Remaining L0 provenance obligation after this export. -/
def BoundedRecognitionCouplingObligation : String :=
  "Force a production RecognitionStructure.R (or lattice adjacency) to satisfy \
BoundedRecognitionRelation at a fixed radius from Recognition dynamics; then \
transport nonzero pair weights through RelationSupportsWeight to FiniteRange."

What this page does not claim

FiniteRange is forced by Recognition Science from first principles. The all-true relation is the only relation that fails to force FiniteRange. The band geometry is derived from Recognition dynamics rather than chosen as a 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: