pointInterface_at_ref
plain-language theorem explainer
The point interface, the minimal two-outcome recognizer that returns 1 exactly on a chosen reference element, evaluates to 1 at that reference. Researchers building the primitive-observer layer of Recognition Science cite it when showing that a single named distinction induces a separating finite recognizer. The proof is a direct unfolding of the interface definition followed by simplification of the conditional.
Claim. Let $K$ be any type and let $x_0$ be an element of $K$. Then the observation map of the two-outcome point interface at $x_0$ satisfies $f(x_0)=1$ where $f$ returns the nonzero element of Fin 2 precisely when its argument equals $x_0$.
background
The module establishes that non-trivial recognition forces an interface and that an interface is the primitive observer. The point interface is defined as the canonical two-outcome structure on any carrier $K$ whose observation map returns 1 on the reference element $x_0$ and 0 elsewhere; it is the minimal finite recognizer induced by one named distinction. This construction rests on the PrimitiveInterface record and on the structural conditions extracted from the seven axioms of PrimitiveDistinction.
proof idea
The term proof unfolds the pointInterface definition, exposing the if-then-else clause of the observe map, then applies simp to reduce the equality at the reference point to the true branch.
why it matters
The result is invoked by pointInterface_separates to establish that the interface separates any distinct pair. It supplies the concrete finite recognizer required by the module's claim that non-trivial recognition forces a primitive observer, supplying the pre-physical floor before later modules upgrade the structure to ledger configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.