cell_eq_iff_kernel
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Geometry rebuilt as a quotient of what measurements can distinguish
"Theorem 1: The induced map R̄ : C_R → E is injective. ... distinct observable states correspond to distinct events, and no further distinctions exist within C_R beyond those encoded by R"