every_cell_has_label
plain-language theorem explainer
Every cell in the recognition lattice generated by a primitive interface carries a label from the finite observation codomain. Researchers assembling the pre-spatial structure in Recognition Science cite this when verifying that quotient cells inherit finite resolution. The proof is a direct term construction that selects the label via cellLabel and confirms neighborhood membership by simplification.
Claim. Let $I$ be a primitive interface on carrier $K$ with finite codomain size $n = I.n$. For any cell $c$ in the recognition lattice (the quotient of $K$ by the kernel equivalence induced by $I$), there exists a label $l$ in Fin $n$ such that $c$ belongs to the neighborhood of $l$.
background
The recognition lattice is the quotient of the carrier by the interface setoid, whose cells are the equivalence classes of configurations indistinguishable under the observe map of the interface. A primitive interface supplies a positive integer $n$ and a map from the carrier to Fin $n$, thereby fixing finite resolution at the level of events. This module converts the structural claim of Recognition Geometry into theorems by showing that any such quotient inherits labeled neighborhoods from the finite codomain.
proof idea
The proof is a one-line term wrapper. It refines the existential to the witness cellLabel I c and then applies simp on the neighborhood predicate to discharge the membership goal.
why it matters
This result populates the every_cell_labeled field inside recognitionLatticeCert, the central certificate that collects existence from nontrivial recognition, kernel equivalence, and the LogicNat interpretation. It completes the finite-resolution step required by the Recognition Geometry claim in the module, ensuring the pre-spatial lattice carries the event codomain without metric or topological assumptions. In the larger framework it bridges PrimitiveDistinction to the lattice structure that later supports the eight-tick octave and spatial dimension derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.