Foundation Pair Kernel Bounded Coupling Bounded Recognition Coupling Obligation

A boundary on what the framework forces

In Recognition Science, a recognition event is a discrete record that one thing in a system marks another. The framework's foundational structure, called RecognitionStructure, plus a valid tick (a step in that discrete record) are the bare minimum ingredients. The theorem BoundedRecognitionCouplingObligation_not_forced_by_bare_RS establishes a boundary: these bare ingredients do not force a condition called bounded coupling, which would require that any two things that recognize each other are within some fixed distance. The machine-checked library of formal theorems proves this by constructing a valid carrier where the recognition relation is all-true, meaning every element recognizes every other, and where the associated mean-field weights fail both the bounded relation and the finite-range condition for any chosen radius.

The proof is a closed negative. It does not say bounded coupling is impossible; it says it is not a consequence of the framework's most basic axioms. The theorem constructs, for any radius, a system with a valid tick where the mean-field weight graph has nonzero weights between elements that are arbitrarily far apart. This coexists with a valid AtomicTick, so the obstruction is not a contradiction but a genuine gap. The framework's own library banks this as a theorem, not a hypothesis, because the existence of such a counterexample is what is proved.

What this does not claim is that bounded coupling is false or irrelevant. It only claims the bare structure does not force it. The library then opens a separate, positive route: a metric-generalized export where a recognition relation contained in a closed metric ball does force finite-range weights. This is a theorem for any metric, not just a one-dimensional distance. The original one-dimensional export becomes a special case of this more general statement.

For the three-dimensional lattice geometry already committed to in the framework's Door-2 work, the library proves that the box weight is finite-range in the encoded ℓ¹ metric at radius 1. This is an inhabitant of the metric export, but it is not forced by bare RecognitionStructure; it is a positive geometry chosen for that work. The remaining premise, named ProductionLatticeCouplingObligation, is to force or commit production pair-weight support onto a metric-bounded recognition relation equivalent to the three-dimensional nearest-neighbor lattice. Until that premise is derived from deeper recognition dynamics, the global one-dimensional finite-range condition remains a hypothesis, not a theorem.

The consequence is a clear map of what the framework knows and what it has chosen. The theorem draws a line: bare recognition plus a tick does not buy bounded coupling. The metric export shows what additional structure is needed, and the three-dimensional lattice is a concrete choice that satisfies it, but that choice is a model, not a forced result. The reader can now see that the framework's path to three-dimensional locality rests on a named, open obligation, not on a hidden assumption.

/-- 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⟩

/-- **THEOREM (closed negative).** Bare `RecognitionStructure` (via
`tickCarrier`, whose `R` is all-true) plus a valid `AtomicTick` coexist with
mean-field weights that fail both `BoundedRecognitionRelation` and
`FiniteRange`. This is the Lean form of the season-1 obstruction. -/
theorem recognitionStructure_atomicTick_do_not_force_boundedCoupling
    (radius : ℕ) :
    ∃ n : ℕ,
      Nonempty (AtomicTick (tickCarrier n)) ∧
        ¬ BoundedRecognitionRelation (tickCarrier n).R radius ∧
          RelationSupportsWeight (tickCarrier n).R (meanFieldWeight n) ∧
            ¬ FiniteRange (meanFieldWeight n) radius := by
  refine ⟨radius + 2, ⟨scheduleAtomicTick (fun _ => ⟨0, by omega⟩)⟩, ?_,
    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

/-- **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

/-- Direct form: `boxWeight` is finite-range in the encoded ℓ¹ metric. -/
theorem boxWeight_finiteRangeOn (L : ℕ) :
    FiniteRangeOn (boxWeight L) (encodedDist3 L) 1 :=
  (boxWeight_finiteRangeOn_export_v1 L).2.2

/-- 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

Bounded coupling is false or impossible, only that it is not forced by the bare structure. The three-dimensional lattice geometry is derived from first principles; it is a committed model. The global one-dimensional finite-range condition is a theorem; it remains a hypothesis.

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: