Separates

formal source

  82
  83/-- An interface separates a pair if the pair lands in distinct observed
  84outcomes. -/
  85def Separates {K : Type*} (I : PrimitiveInterface K) (x y : K) : Prop :=
  86  I.observe x ≠ I.observe y
  87
  88/-- The canonical two-outcome interface that asks whether the input is the
  89chosen reference point `x₀`. This is the minimal finite recognizer induced by
  90one named distinction. -/
  91noncomputable def pointInterface {K : Type*} (x₀ : K) :
  92    PrimitiveInterface K where
  93  n := 2
  94  hpos := by norm_num
  95  observe := fun x =>
  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