Foundation Recognition Lattice From Recognizer Cell Eq Iff Kernel

The kernel equivalence

In mathematics, an equivalence relation groups the elements of a set into disjoint classes, where two elements belong to the same class exactly when the relation holds between them. The theorem cell_eq_iff_kernel states this same principle for a recognizer: two configurations produce the same cell in the recognition lattice if and only if the recognizer's kernel relation holds between them. The kernel relation is the primitive observer's indistinguishability relation, the formal way of saying that the recognizer cannot tell the two configurations apart.

The proof is a direct application of the standard fact that the quotient of a set by an equivalence relation identifies exactly the elements that are related. In the framework's machine-checked library of formal theorems, the declaration is literally the quotient equality theorem applied to the recognizer's kernel. The result is that the recognition lattice, defined as the set of equivalence classes of configurations under the kernel, has cells that correspond precisely to the indistinguishability classes of the recognizer.

The theorem does not claim that the lattice is a metric space, a topological manifold, or a geometric object with distances and shapes. It establishes only the pre-spatial quotient structure: a discrete collection of cells, each labeled by a finite observation outcome. The framework's own documentation is explicit that this lattice is not yet a manifold, and that the map from the universal iteration object into a finite lattice may collapse distinct elements, just as a parity check collapses the natural numbers into two classes.

What the theorem provides is the foundational identification that makes the rest of the framework's spatial claims possible. It is the bridge from the primitive notion of a recognizer, which merely observes and labels, to the first structural object, a lattice of cells that the recognizer cannot distinguish. This is the starting point for building neighborhoods, and eventually geometry, from the raw material of recognition events.

/-- Two configurations determine the same cell iff the recognizer cannot
distinguish them. -/
theorem cell_eq_iff_kernel {K : Type*} (I : PrimitiveInterface K) (x y : K) :
    cellOf I x = cellOf I y ↔ I.kernel x y := by
  exact Quotient.eq

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

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

What this page does not claim

The theorem does not claim the lattice has any geometric or metric structure. It does not claim that the map from the universal iteration object into a finite lattice is injective. It does not establish the physical recognition-to-linking bridge that would connect this lattice to three-dimensional space.

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: