pointInterface_separates
plain-language theorem explainer
The point interface at reference x₀ separates x₀ from any distinct y by returning different observed outcomes. Foundational derivations of observers from recognition cite this to confirm the minimal two-outcome recognizer distinguishes a pair once a distinction exists. The proof unfolds the separation predicate, rewrites via the interface evaluations at and away from the reference, and normalizes the resulting inequality.
Claim. Let $K$ be any type and let $x_0, y$ be distinct elements of $K$. Let $I$ be the canonical two-outcome interface that returns true precisely when its input equals the fixed reference $x_0$. Then the observed value of $x_0$ under $I$ differs from the observed value of $y$ under $I$.
background
The module proves that non-trivial recognition forces a finite interface, which supplies the primitive observer. Separates is the predicate that an interface $I$ distinguishes a pair when $I$ applied to the first element differs from $I$ applied to the second. pointInterface is the minimal recognizer that checks equality to one chosen reference point $x_0$ and yields a two-valued outcome space.
proof idea
Unfold Separates to expose the inequality on observations. Rewrite the left side with pointInterface_at_ref to obtain the reference case. Introduce the symmetric inequality y ≠ x₀ from the hypothesis. Rewrite the right side with pointInterface_away. Normalize the resulting Boolean inequality to close the goal.
why it matters
This lemma is invoked inside nontrivial_recognition_forces_interface, the central theorem asserting that any non-trivial recognition yields a separating interface and hence a primitive observer. It realizes the pre-physical observer step: observer dependence appears at the first distinction event rather than at a later measurement layer. The result sits upstream of RecognizerInducesLogic and supplies the interface existence needed for the Recognition Composition Law applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.