Foundation Recognition Lattice From Recognizer

The recognition lattice

A recognizer, in the broadest sense, is any process that assigns a label to an input. Two inputs that receive the same label are, from that recognizer's point of view, indistinguishable. Grouping all inputs that share a label into a single cell produces a set of cells: the recognizer's view of its own world. In Recognition Science, the framework's library of machine-checked formal theorems proves that for any primitive interface, a recognizer's kernel-equivalence classes form a lattice, a structure it calls the recognition lattice.

The lattice is pre-spatial. It is not yet a metric or topological manifold, and it does not carry distances or continuity. What it does carry is the recognizer's own resolution: each cell is a class of configurations that the recognizer cannot tell apart. The framework proves that every cell has a label, that a cell's label matches the observation that produced it, and that two cells are equal exactly when their inputs are kernel-equivalent. Finite resolution is inherited from the finite event codomain, so a two-outcome recognizer yields a two-cell lattice.

The central existence theorem, nontrivial_recognition_forces_lattice, states that any non-trivial recognition event forces the existence of such a lattice. The framework also proves uniqueness: interfaces with the same kernel produce canonically equivalent lattices. The universal iteration object LogicNat, which represents repeated application of a step function, maps into the lattice, though the map is an interpretation, not an injection: a finite lattice can collapse distinct iteration steps into the same cell, just as Boolean parity collapses even and odd counts.

In Recognition Science, the recognition lattice is the first structural object to emerge from a recognizer alone, before any geometry is imposed. It establishes that the act of distinguishing inputs, and failing to distinguish them, already organizes the carrier into a well-defined mathematical structure. The framework's library proves this for any primitive interface, and the lattice is the foundation on which later spatial structure is built.

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

/-- A non-trivial recognition event forces a recognition lattice. -/
theorem nontrivial_recognition_forces_lattice (K : Type*) :
    NontrivialRecognition K →
    ∃ (I : PrimitiveInterface K), Nonempty (RecognitionLattice I) := by
  intro h
  obtain ⟨I, x, _y, _hdist, _hsep⟩ := nontrivial_recognition_forces_interface K h
  exact ⟨I, ⟨cellOf I x⟩⟩

/-- If two interfaces have the same kernel, then their recognition lattices
are canonically equivalent. -/
noncomputable def latticeEquivOfSameKernel {K : Type*}
    (I J : PrimitiveInterface K) (h : SameKernel I J) :
    RecognitionLattice I ≃ RecognitionLattice J where
  toFun := Quotient.map (fun x => x) (by
    intro x y hxy
    exact (h x y).mp hxy)
  invFun := Quotient.map (fun x => x) (by
    intro x y hxy
    exact (h x y).mpr hxy)
  left_inv := by
    intro c
    refine Quotient.inductionOn c ?_
    intro x
    rfl
  right_inv := by
    intro c
    refine Quotient.inductionOn c ?_
    intro x
    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 recognition lattice is not a metric or topological space. The LogicNat map into a finite lattice is not an embedding. This module does not derive the golden ratio or the cost function.

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: