pointInterface_separates

formal source

 108  simp [h]
 109
 110/-- The point interface separates any point from any distinct point. -/
 111theorem pointInterface_separates {K : Type*} {x₀ y : K} (h : x₀ ≠ y) :
 112    Separates (pointInterface x₀) x₀ y := by
 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. -/
 129theorem nontrivial_recognition_forces_interface (K : Type*) :
 130    NontrivialRecognition K →
 131    ∃ (I : PrimitiveInterface K) (x y : K),
 132      equalityDistinction K x y ∧ Separates I x y := by
 133  intro h
 134  rcases h with ⟨x, y, hxy⟩
 135  exact ⟨pointInterface x, x, y, hxy, pointInterface_separates hxy⟩
 136
 137/-- Same theorem under the observer name: non-trivial recognition forces a
 138primitive observer. -/
 139theorem nontrivial_recognition_forces_observer (K : Type*) :
 140    NontrivialRecognition K →
 141    ∃ (O : PrimitiveObserver K) (x y : K),