  96    if x = x₀ then (1 : Fin 2) else (0 : Fin 2)
  97
  98/-- The point interface recognizes its reference point as outcome `1`. -/
  99theorem pointInterface_at_ref {K : Type*} (x₀ : K) :
 100    (pointInterface x₀).observe x₀ = (1 : Fin 2) := by
 101  unfold pointInterface
 102  simp
 103
 104/-- Any point distinct from the reference is recognized as outcome `0`. -/
 105theorem pointInterface_away {K : Type*} {x₀ y : K} (h : y ≠ x₀) :
 106    (pointInterface x₀).observe y = (0 : Fin 2) := by
 107  unfold pointInterface
 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*) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.