Foundation Recognition Lattice From Recognizer Lattice Equiv Of Same Kernel Cell

The kernel equivalence

A recognizer is a device that sorts a collection of possible configurations into a finite set of outcomes. Two configurations are indistinguishable to it when it assigns them the same outcome. The kernel of a recognizer is the relation that holds between two configurations exactly when the recognizer cannot tell them apart. This relation is an equivalence relation: it is reflexive, symmetric, and transitive, so it partitions the configurations into disjoint cells, where each cell is a maximal set of mutually indistinguishable configurations.

The declaration latticeEquivOfSameKernel_cell states the following. Suppose two recognizers, call them I and J, have the same kernel: for every pair of configurations, I cannot tell them apart if and only if J cannot tell them apart. Then the theorem says that the cell containing a configuration x in the partition produced by I is mapped, by a canonical bijection, exactly to the cell containing x in the partition produced by J. The proof is a definitional equality: the map sends the cell of x under I to the cell of x under J, and this is true by the way the map is defined. In plain terms, if two recognizers make exactly the same distinctions, then their pictures of the world are the same picture, just with the cells named by the outcomes of one or the other.

This is a statement about the recognition quotient lattice, the collection of cells together with the structure inherited from the outcome labels. The theorem does not claim that the two recognizers assign the same labels to the same cells. It does not claim that the cells are points in a space with distance or topology. It does not claim that the map is an injection into the natural numbers or any other infinite object. The lattice can be finite, as with a two-outcome recognizer, and the theorem remains true. The theorem is a statement of uniqueness up to canonical equivalence: the structure of indistinguishability is what matters, not the names of the outcomes.

In the framework of Recognition Science, this theorem is a piece of the structural claim that a recognizer's kernel-equivalence classes are the first lattice. It establishes that the lattice is well-defined: it does not depend on which recognizer with a given kernel you happen to choose. The practical consequence is that when two observers make the same distinctions, they are guaranteed to be talking about the same underlying cells, even if their labels differ. This is the sense in which the framework's account of structure is observer-independent at the level of indistinguishability.

/-- The canonical equivalence sends each cell to the cell of the same
configuration. -/
theorem latticeEquivOfSameKernel_cell {K : Type*}
    (I J : PrimitiveInterface K) (h : SameKernel I J) (x : K) :
    latticeEquivOfSameKernel I J h (cellOf I x) = cellOf J x := rfl

/-- The setoid induced by a primitive interface. Two configurations are
equivalent iff the interface sends them to the same event. -/
def interfaceSetoid {K : Type*} (I : PrimitiveInterface K) : Setoid K where
  r := I.kernel
  iseqv := kernel_is_equivalence I

/-- The canonical equivalence sends each cell to the cell of the same
configuration. -/
theorem latticeEquivOfSameKernel_cell {K : Type*}
    (I J : PrimitiveInterface K) (h : SameKernel I J) (x : K) :
    latticeEquivOfSameKernel I J h (cellOf I x) = cellOf J x := rfl

What this page does not claim

The theorem does not claim the two recognizers produce identical labels for corresponding cells. It does not claim the recognition quotient lattice is a manifold or carries a metric or topology. It does not claim the map from the iteration object LogicNat to the lattice is an embedding or injection.

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: