cellLabel_cellOf
The theorem states that the label of the cell generated from any element x equals the direct observation of x under a primitive interface. Researchers constructing the recognition quotient lattice cite it to simplify expressions that alternate between cell formation and label extraction. The proof holds by reflexivity because cellOf and cellLabel are defined to be inverses on the observation map.
claimLet $I$ be a primitive interface on carrier $K$. For any $x$ in $K$, the label of the cell of $x$ satisfies $cellLabel(I, cellOf(I, x)) = I.observe(x)$.
background
The module builds the recognition quotient lattice as the partition of the carrier into kernel-equivalence classes induced by a primitive observer. A primitive interface supplies an observation map from the carrier to a finite label set; cellOf returns the equivalence class containing a given element, and cellLabel returns the shared label of that class. This construction yields finite-resolution neighborhoods directly from event labels and remains pre-spatial until metric structure is imposed later.
proof idea
The proof is a one-line term that applies reflexivity. Because the definitions of cellOf and cellLabel are constructed so that the label of the generated cell is definitionally identical to the original observation, the equality is immediate.
why it matters in Recognition Science
The result supplies the basic round-trip identity that confirms labels are preserved under the quotient map, thereby supporting the module claim that kernel classes constitute the first recognition lattice. It sits inside the pre-spatial stage of the Recognition Geometry development and is consistent with the forcing chain that later forces D=3. No downstream uses are recorded yet, leaving its role as a simplification lemma for later lattice manipulations.
scope and limits
- Does not introduce metric or topological structure on the lattice.
- Does not treat infinite carriers or continuous observation maps.
- Does not prove embedding of LogicNat when the label set is finite.
- Does not connect to the phi-ladder, constants, or physical forcing steps.
formal statement (Lean)
78@[simp] theorem cellLabel_cellOf {K : Type*} (I : PrimitiveInterface K) (x : K) :
79 cellLabel I (cellOf I x) = I.observe x := rfl
proof body
Term-mode proof.
80
81/-- A finite-resolution neighborhood: all cells with a given observed label. -/