cellOf
plain-language theorem explainer
cellOf sends a configuration x under primitive interface I to its equivalence class in the recognition lattice, the quotient of the carrier by the kernel of I. Researchers constructing pre-spatial structure from finite-resolution observers would cite this when forming the basic cells of the lattice. The definition is realized by a direct application of the quotient constructor to the interface setoid.
Claim. For a primitive interface $I$ on carrier $K$, the cell containing configuration $x$ is the equivalence class $[x]$ in the quotient $K / {}_I$, where $x {}_I y$ holds precisely when $I$ maps $x$ and $y$ to the same element of its finite codomain.
background
The module builds the recognition lattice as the quotient of configurations by the indistinguishability kernel of a primitive observer. A primitive interface consists of a positive integer $n$ together with an observation map $K$ to Fin $n$, supplying finite resolution. The recognition lattice is the quotient of $K$ by the interface setoid, whose relation identifies configurations sent to the same observed event.
proof idea
The definition is a one-line wrapper that applies Quotient.mk to the interface setoid of I on the input configuration x.
why it matters
This supplies the cell constructor used by cell_eq_iff_kernel (cells coincide exactly when the kernel relates the configurations) and by logicNat_interprets_into_lattice (every primitive interface admits an interpretation of LogicNat into its lattice). It realizes the module claim that kernel-equivalence classes form the first recognition lattice, the pre-spatial quotient before metric or dimensional structure appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.