cellLabel
plain-language theorem explainer
The cell label function extracts the finite observed event from each equivalence class in the recognition lattice. Researchers constructing discrete event spaces from a recognizer cite it to obtain well-defined labels on quotient cells. The definition lifts the interface observation map through the quotient, which succeeds because the equivalence relation coincides exactly with the kernel of that map.
Claim. Let $I$ be a primitive interface with observation map $o:K→ Fin(n)$. Let $L_I$ be the quotient of $K$ by the kernel equivalence $x∼y$ iff $o(x)=o(y)$. The label map $ℓ:L_I→ Fin(n)$ is the unique function satisfying $ℓ([x])=o(x)$ for every configuration $x$.
background
A primitive interface consists of a positive integer $n$ and an observation map from the carrier to the finite set $Fin(n)$, encoding finite-resolution distinguishable events. The recognition lattice is the quotient of the carrier by the kernel of this map, so cells are precisely the sets of configurations that the interface cannot distinguish.
proof idea
The definition is a one-line wrapper that applies Quotient.lift to the observe function of the interface. The required compatibility condition holds by construction of the interface setoid, which equates configurations precisely when they share the same observed label.
why it matters
This definition supplies the label extraction used by every_cell_has_label and neighborhood to equip the lattice with finite-resolution structure. It realizes the module claim that the recognition quotient inherits finite event labels from the interface codomain, forming the pre-spatial lattice that precedes metric or dimensional emergence in the Recognition Geometry construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.