cell_eq_iff_kernel
The equivalence states that two configurations x and y on carrier K induce identical recognition cells under primitive interface I precisely when I's kernel relation holds between them. Researchers constructing the initial quotient lattice from finite-resolution observers in Recognition Science cite this result when identifying cells with indistinguishability classes. The proof is a direct one-line application of the quotient equality rule to the cellOf definition.
claimLet $I$ be a primitive interface on carrier $K$. For configurations $x,y:K$, the cells satisfy cellOf$(I,x)=$cellOf$(I,y)$ if and only if the kernel of $I$ holds between $x$ and $y$.
background
The module realizes the recognition lattice as the quotient of the configuration space $K$ by the indistinguishability kernel of any primitive interface. A primitive interface supplies a positive integer $n$ and an observation map $K$ to Fin $n$; its kernel is the relation of equal observations. The cellOf constructor yields the corresponding equivalence class in the quotient. Upstream results include the PrimitiveInterface structure, which encodes the finite-resolution recognizer, and kernel definitions from cosmology that generalize the same indistinguishability idea. The local theoretical setting is the pre-spatial recognition quotient lattice, which inherits finite resolution from the event codomain but carries no metric or topology yet.
proof idea
The proof is a one-line term that invokes Quotient.eq, the canonical equality principle for the quotient type that underlies the cellOf construction.
why it matters in Recognition Science
This supplies the fundamental equivalence identifying cells of the recognition lattice exactly with the kernel classes of the observer, thereby realizing the module claim that a recognizer's kernel-equivalence classes form the first recognition lattice. It fills the initial structural step in the Recognition Geometry program before neighborhoods, labels, and the LogicNat interpretation are introduced. In the broader framework it marks the transition from raw recognition events to the pre-spatial lattice that later supports the forcing chain and emergence of three-dimensional structure.
scope and limits
- Does not equip the lattice with a metric or topology.
- Does not extend the construction to infinite-resolution observers.
- Does not derive physical constants, dimensions, or dynamics from the lattice.
- Does not address interfaces beyond the primitive finite-event form.
formal statement (Lean)
64theorem cell_eq_iff_kernel {K : Type*} (I : PrimitiveInterface K) (x y : K) :
65 cellOf I x = cellOf I y ↔ I.kernel x y := by
proof body
Term-mode proof.
66 exact Quotient.eq
67
68/-! ## Finite-resolution labels and neighborhoods -/
69
70/-- The finite event label of a recognition cell. This is well-defined because
71the quotient identifies exactly configurations with equal observed labels. -/