Foundation Recognition Lattice From Recognizer Recognition Lattice Cert Inhabite

The recognition lattice

A recognition lattice is a discrete record of events: a set of cells, each cell holding all the configurations a recognizer cannot tell apart. The declaration recognitionLatticeCert_inhabited is a machine-checked theorem stating that for any type of configurations, such a lattice exists. It is a certificate, a packaged proof that the lattice is always there when the recognizer is.

The theorem builds the lattice from a primitive interface, a recognizer with a finite set of possible observations. Two configurations land in the same cell exactly when the recognizer produces the same observation for both. This is a quotient construction: the recognizer's indistinguishability relation carves the full set of configurations into cells. The proof shows the cells are well-defined, that every cell carries a label, and that the recognizer's own observations give each cell a finite-resolution neighborhood.

The certificate bundles five properties into one object. From any non-trivial recognition event, a lattice exists. The kernel relation is an equivalence. Every cell has a label. Interfaces with the same kernel produce equivalent lattices. And the universal iteration object maps into the lattice. The last map is an interpretation, not an embedding: a finite lattice can collapse the infinite iteration structure, just as a parity check collapses the natural numbers into two classes.

What the theorem does not claim is as precise as what it proves. The lattice is pre-spatial. It is not a metric or topological manifold, and it carries no geometry. The map from the iteration object is not injective, so the lattice does not contain a copy of the free iteration structure. The theorem guarantees existence and structure, not any particular size or shape of the lattice. A two-outcome recognizer produces a two-cell lattice; the theorem is silent on which recognizer is the right one for physics.

theorem recognitionLatticeCert_inhabited (K : Type*) :
    Nonempty (RecognitionLatticeCert K) :=
  ⟨recognitionLatticeCert K⟩

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

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

/-- Every lattice cell has a finite-resolution label. -/
theorem every_cell_has_label {K : Type*} (I : PrimitiveInterface K)
    (c : RecognitionLattice I) :
    ∃ label : Fin I.n, c ∈ neighborhood I label := by
  refine ⟨cellLabel I c, ?_⟩
  simp [neighborhood]

/-- 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 lattice is not a metric or topological manifold. The map from the iteration object is not an embedding, so the lattice does not contain a copy of the free iteration structure. The theorem does not identify which recognizer is the physical one.

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: