pointInterface_separates
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of non-trivial recognition on a given carrier.
- Does not extend separation to carriers without a distinguished reference point.
- Does not derive physical measurement or quantum postulates.
- Does not address interfaces with resolution greater than two.
formal statement (Lean)
111theorem pointInterface_separates {K : Type*} {x₀ y : K} (h : x₀ ≠ y) :
112 Separates (pointInterface x₀) x₀ y := by
proof body
Term-mode proof.
113 unfold Separates
114 rw [pointInterface_at_ref x₀]
115 have hy : y ≠ x₀ := fun h' => h h'.symm
116 rw [pointInterface_away hy]
117 norm_num
118
119/-! ## Main Theorem -/
120
121/-- **Observer from recognition.**
122
123If a carrier admits any non-trivial recognition, then there exists a finite
124interface, hence a primitive observer, that separates a distinguished pair.
125
126This is the pre-physical observer theorem: observer-dependence is not added
127at the quantum-measurement layer. It is forced at the first moment a
128distinction becomes an event. -/