pointInterface_separates
plain-language theorem explainer
The theorem shows that the point interface at reference element x0 separates x0 from any distinct y in carrier K. Researchers deriving observer structures from recognition events cite this to ground separation from a single named distinction. The proof is a direct term reduction that unfolds the separation predicate and applies the reference and away cases of the point interface.
Claim. Let $K$ be any type and let $x_0, y$ be distinct elements of $K$. The canonical two-outcome interface at $x_0$ (which returns whether its input equals $x_0$) satisfies that its observation of $x_0$ differs from its observation of $y$.
background
The module proves that non-trivial recognition forces a primitive observer via a finite interface. Separates holds for interface I and pair x,y precisely when I.observe x differs from I.observe y. pointInterface is the minimal two-outcome recognizer that checks equality to a fixed reference point x0, as defined in the sibling declarations of this module.
proof idea
The proof is a term-mode reduction. It unfolds Separates, rewrites the reference observation via pointInterface_at_ref, derives y ≠ x0 by symmetry of the given inequality, applies pointInterface_away to the distinct case, and closes with norm_num.
why it matters
This lemma is invoked by nontrivial_recognition_forces_interface, the module's main result that any non-trivial recognition induces a separating interface and hence a primitive observer. It supplies the pre-physical step in which observer-dependence appears at the first distinction event, before quantum layers or physical constants enter. The module doc-comment identifies this as the floor for later upgrades to finite-resolution recognizers over ledger configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.