Foundation Pair Kernel Bounded Coupling Box Weight Supported On Lattice3

Bounded coupling on a lattice

A recognition event, a discrete record of a pair of items being compared, can be modeled as a link between two points in a graph. The question is whether those links can stay short-ranged, or whether they must stretch across the whole system. The declaration boxWeight_supported_on_lattice3 answers this for one specific, committed geometry: a three-dimensional cubic lattice of side length L, where each point is connected only to its nearest neighbors.

The theorem proves that a particular weight assignment, called boxWeight, has a key property. Whenever the weight between two lattice points is nonzero, those points are within a distance of 1 in the lattice's own metric, the ℓ¹ distance after encoding the three-dimensional coordinates into a flat index. In plain terms, every nonzero connection in this model is a nearest-neighbor connection. This is a finite-range property: no weight reaches beyond the immediate shell of neighbors.

The proof is direct. The weight is defined as 1 when the encoded distance is at most 1, and 0 otherwise. The theorem simply unpacks that definition and verifies the support condition. It is a THEOREM in the machine-checked library of formal theorems, with no unproved assumptions. It is the positive half of a larger result that also shows a contrasting mean-field weight, which connects every pair equally, fails this same finite-range test on the same lattice.

In Recognition Science, this result matters because it shows one viable route to three-dimensional locality. The framework's bare structure, a recognition relation plus a valid tick, does not by itself force bounded coupling; a separate theorem in the same module proves that counterexample exists. The lattice result instead assumes the lattice geometry as a committed choice, called lattice3RecognitionStructure, and shows that under that choice the box weight is well-behaved. The gap between the bare rules and this committed geometry is named as an open obligation, not a derived fact.

What the theorem does not claim is just as important. It does not prove that the lattice geometry is forced by the framework's axioms. It does not establish that any production weight graph must be supported on this lattice. It does not identify the lattice with any physical system, such as a protein or a crystal. The theorem is a conditional guarantee: if you choose this geometry, then this weight is local. The unconditional claim, that recognition dynamics alone produce this lattice, remains a hypothesis.

theorem boxWeight_supported_on_lattice3 (L : ℕ) :
    RelationSupportsWeightOn (lattice3RecognitionRelation L) (boxWeight L) := by
  intro i j hne
  dsimp [lattice3RecognitionRelation, encodedDist3]
  change (if dist3 ((enc3 L).symm i) ((enc3 L).symm j) ≤ 1 then (1 : ℝ) else 0) ≠ 0 at hne
  split_ifs at hne with hle
  · exact hle
  · exact (hne rfl).elim

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

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

What this page does not claim

The lattice geometry is forced by the framework's basic axioms. The box weight is the unique weight satisfying the finite-range property. The theorem identifies the lattice with any specific physical system.

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: