Foundation Pair Kernel Bounded Coupling Finite Range Export V1 Of Finite Range O

The metric export

In the Recognition Science framework, a ledger (a discrete record of events) assigns a weight to every pair of entries. The question at stake is whether those weights can reach arbitrarily far across the index set, or whether they die out beyond some radius. The declaration finiteRange_export_v1_of_finiteRangeOn answers that question for a generalized setting: it proves that if the recognition relation is bounded in some metric, and the weights are supported on that relation, then the weights are finite-range in that same metric.

The proof is short and structural. It assumes two premises. First, the recognition relation is contained in a closed metric ball of some radius: any two entries that recognize each other are at distance at most that radius. Second, the weight graph is supported on the relation: any nonzero weight implies the two entries recognize each other. From these, the theorem derives that any pair of entries farther apart than the radius must have weight zero. The argument is a contraposition: if the weight were nonzero, support would force recognition, and boundedness would force the distance to be within the radius, contradicting the assumption that it is farther.

The declaration is the metric-parametric form of an earlier 1D export. The original version used a specific distance function, cellDist, which works for a one-dimensional chain. The generalized version, finiteRangeOn_export_v1, accepts an arbitrary index metric, so it can apply to higher-dimensional lattices. The 1D case is recovered as the special instance where the metric is cellDist. This matters because the framework's committed three-dimensional carrier uses an encoded ℓ¹ distance on a box lattice, not the raw index distance, and the metric export is what makes the locality claim meaningful there.

In Recognition Science, this theorem is part of a larger structure. The framework's machine-checked library of formal theorems also proves a closed negative: bare recognition structure plus a valid atomic tick do not force bounded coupling. There exist carriers with an all-true recognition relation, supporting mean-field weights, that fail both boundedness and finite range. That negative result is what motivates the metric-generalized export: it shows the bounded-coupling obligation cannot be discharged from the bare axioms alone, and the export provides a route when a metric is committed.

What the declaration does not claim is equally important. It does not prove that finite range is forced by recognition structure alone; that remains an open hypothesis. It does not identify the metric or the radius; those are premises. And it does not establish that the three-dimensional lattice geometry is forced from deeper dynamics. The D=3 inhabitant, boxWeight, is a committed model geometry, not a derivation from first principles. The theorem licenses a conditional statement: given a bounded metric and supported weights, finite range follows. It leaves open the production obligation of forcing that metric-bounded support from deeper recognition dynamics.

/-- **finiteRangeOn_export_v1.** Metric-parametric form of
`finiteRange_export_v1`. -/
theorem finiteRangeOn_export_v1
    {n radius : ℕ} {R : Fin n → Fin n → Prop}
    {dist : Fin n → Fin n → ℕ} {G : WeightedLedgerGraph n}
    (hB : BoundedRecognitionRelationOn R dist radius)
    (hS : RelationSupportsWeightOn R G) :
    FiniteRangeOn G dist radius := by
  intro i j hfar
  by_contra hne
  have hR : R i j := hS i j hne
  have hle : dist i j ≤ radius := hB i j hR
  exact (not_lt_of_ge hle) hfar

/-- Bundle alias matching the named season obligation string. -/
theorem BoundedRecognitionCouplingObligation_not_forced_by_bare_RS
    (radius : ℕ) :
    ∃ n : ℕ,
      Nonempty (AtomicTick (tickCarrier n)) ∧
        ¬ BoundedRecognitionRelation (tickCarrier n).R radius ∧
          ¬ FiniteRange (meanFieldWeight n) radius := by
  rcases recognitionStructure_atomicTick_do_not_force_boundedCoupling radius with
    ⟨n, hTick, hB, _hS, hFR⟩
  exact ⟨n, hTick, hB, hFR⟩

/-- Strengthened recognition structure for the Door-2 D=3 carrier.
This commits `R` to the ℓ¹ unit ball. It is NOT derived from bare
`RecognitionStructure`; forcing that commitment is
`ProductionLatticeCouplingObligation`. -/
def lattice3RecognitionStructure (L : ℕ) : RecognitionStructure where
  U := Fin (L * L * L)
  R := lattice3RecognitionRelation L

What this page does not claim

FiniteRange is forced by recognition structure alone. The metric or the radius is identified by the theorem. The three-dimensional lattice geometry is derived from first principles.

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/PairKernelBoundedCoupling.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: