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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.