pointInterface_away
plain-language theorem explainer
The theorem states that the point interface for reference x₀ maps any distinct input y to outcome 0 in Fin 2. Researchers constructing primitive observers from single distinctions in Recognition Science cite it when verifying separation. The proof is a direct term-mode reduction that unfolds the interface definition and simplifies with the distinctness hypothesis.
Claim. Let $I$ be the point interface for reference point $x_0$, with observe function returning 1 precisely on input equal to $x_0$ and 0 otherwise. Then for any $y$ with $y ≠ x_0$, $I$.observe$(y) = 0$.
background
The module establishes that non-trivial recognition forces a primitive interface that acts as the minimal observer. The pointInterface is the canonical two-outcome recognizer induced by one named distinction: it returns 1 exactly when the input matches the chosen reference $x_0$ and 0 otherwise. This rests on the PrimitiveInterface structure whose observe map is a finite-valued function on the carrier type $K$.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of pointInterface, exposing the conditional that yields 0 on any input unequal to $x_0$, then applies simp with the hypothesis $y ≠ x_0$ to obtain the required equality.
why it matters
This result supplies the away case needed for pointInterface_separates, which in turn shows that the point interface separates the reference from any distinct point. It completes the module's core step that a single distinction induces a finite recognizer, providing the pre-physical floor before later upgrades to ledger configurations. The construction aligns with the framework's derivation of observer-like structure directly from non-trivial recognition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.