Foundation Recognition Lattice From Recognizer Logic Nat Interprets Into Lattice

The lattice interpretation

LogicNat is the framework's name for the universal iteration object: a structure generated by an identity element and a step function, so that its elements behave like the natural numbers 0, 1, 2, and so on. The theorem logicNat_interprets_into_lattice proves that for any primitive interface (a recognizer with a finite set of possible observations) and any choice of a base configuration and a step function on configurations, there exists a map from LogicNat into the recognition lattice. The recognition lattice is the quotient of all configurations by the recognizer's indistinguishability kernel: two configurations occupy the same cell exactly when the recognizer cannot tell them apart. The map sends the identity element to the cell of the base configuration, and sends each successor step to the cell of the stepped configuration.

The force of the theorem is existence and coherence, not uniqueness or injectivity. The map always exists, and it respects the iteration structure: the image of a step is the cell of the stepped configuration. But because the lattice can be finite, for instance with a two-outcome recognizer, distinct natural numbers can land in the same cell. The map is an interpretation, not an embedding. This is the same distinction as the Boolean parity collapse: the iteration object remains free and abstract, while its image in a finite carrier may identify elements that the recognizer cannot separate.

What the theorem does not claim is equally precise. It does not claim that the map is injective, so it does not establish that LogicNat embeds into the lattice. It does not claim that the lattice is infinite, or that it carries a metric or topological structure. The lattice is pre-spatial: it is a quotient by an equivalence relation, with finite-resolution neighborhoods inherited from the finite event labels, but no notion of distance or continuity. The theorem also does not claim that the map is unique; it asserts the existence of at least one such interpretation, and the construction in the proof provides a canonical one.

In the broader framework, this theorem is one component of a certificate that assembles the structural claims of Recognition Geometry: existence of a lattice from any nontrivial recognition event, finite-resolution neighborhoods, uniqueness up to canonical equivalence for interfaces with the same kernel, and the interpretation of LogicNat. The certificate is a single object that packages these results, but the interpretation theorem itself is the narrow claim that the abstract counting structure always finds a home in the lattice, even when that home collapses distinctions.

/-- Every primitive interface admits a `LogicNat` interpretation into its
recognition lattice as soon as a base point and a step function are chosen. -/
theorem logicNat_interprets_into_lattice {K : Type*}
    (I : PrimitiveInterface K) (base : K) (step : K → K) :
    ∃ interp : LogicNat → RecognitionLattice I,
      interp LogicNat.identity = cellOf I base ∧
      ∀ n, interp (LogicNat.step n) =
        cellOf I (step (iteratedCarrier base step n)) := by
  exact ⟨logicNatToLattice I base step, rfl, fun _ => rfl⟩

/-- The **recognition lattice** generated by an interface: the quotient by
the interface kernel. -/
def RecognitionLattice {K : Type*} (I : PrimitiveInterface K) : Type _ :=
  Quotient (interfaceSetoid I)

@[simp] theorem logicNatToLattice_zero {K : Type*}
    (I : PrimitiveInterface K) (base : K) (step : K → K) :
    logicNatToLattice I base step LogicNat.identity = cellOf I base := rfl

@[simp] theorem logicNatToLattice_step {K : Type*}
    (I : PrimitiveInterface K) (base : K) (step : K → K) (n : LogicNat) :
    logicNatToLattice I base step (LogicNat.step n) =
      cellOf I (step (iteratedCarrier base step n)) := rfl

/-- Every primitive interface admits a `LogicNat` interpretation into its
recognition lattice as soon as a base point and a step function are chosen. -/
theorem logicNat_interprets_into_lattice {K : Type*}
    (I : PrimitiveInterface K) (base : K) (step : K → K) :
    ∃ interp : LogicNat → RecognitionLattice I,
      interp LogicNat.identity = cellOf I base ∧
      ∀ n, interp (LogicNat.step n) =
        cellOf I (step (iteratedCarrier base step n)) := by
  exact ⟨logicNatToLattice I base step, rfl, fun _ => rfl⟩

What this page does not claim

The map from LogicNat to the recognition lattice is injective. The recognition lattice is infinite or carries a metric or topological structure. The interpretation map is unique.

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