pointInterface_at_ref
plain-language theorem explainer
The canonical point interface induced by a reference point x₀ in any carrier type K returns the distinguished outcome 1 precisely when its input equals x₀. Workers on the Recognition Science foundation for primitive observers cite this when proving separation of distinguished points. The proof reduces directly to the definition of the interface via unfolding and simplification.
Claim. Let $K$ be any type and let $x_0$ be an element of $K$. Let $I$ be the point interface at $x_0$, the two-outcome recognizer with $I$.observe$(x) = 1$ if $x = x_0$ and $0$ otherwise. Then $I$.observe$(x_0) = 1$ in Fin 2.
background
The module proves that non-trivial recognition forces an interface, which is the primitive observer: the minimal finite-valued recognizer that separates a distinguished pair. The pointInterface is the canonical two-outcome interface that asks whether the input equals the chosen reference point $x_0$. This supplies the pre-physical floor before later modules upgrade the structure to finite-resolution recognizers over ledger configurations.
proof idea
The proof is a one-line wrapper that unfolds the definition of pointInterface and applies simp to reduce the conditional at the reference point.
why it matters
This result is used by pointInterface_separates to establish that the interface separates any point from a distinct reference. It fills the module's core step that non-trivial recognition forces a primitive observer interface. In the Recognition framework it supports the transition from distinctions to observable events ahead of the eight-tick octave and D=3 in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.