pointInterface_at_ref
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any non-trivial distinction inside the carrier.
- Does not construct interfaces with outcome sets larger than two elements.
- Does not address carriers equipped with topology or continuity.
- Does not derive any physical measurement or dynamics.
Lean usage
rw [pointInterface_at_ref x₀]formal statement (Lean)
99theorem pointInterface_at_ref {K : Type*} (x₀ : K) :
100 (pointInterface x₀).observe x₀ = (1 : Fin 2) := by
proof body
Term-mode proof.
101 unfold pointInterface
102 simp
103
104/-- Any point distinct from the reference is recognized as outcome `0`. -/