kernel_is_equivalence

formal source

  66
  67/-- Every primitive interface partitions its carrier into observational
  68equivalence classes. -/
  69theorem kernel_is_equivalence {K : Type*} (I : PrimitiveInterface K) :
  70    Equivalence (I.kernel) :=
  71  ⟨kernel_refl I,
  72   fun {x y} h => kernel_symm I (x := x) (y := y) h,
  73   fun {x y z} h₁ h₂ => kernel_trans I (x := x) (y := y) (z := z) h₁ h₂⟩
  74
  75/-! ## Non-Trivial Recognition -/
  76
  77/-- A carrier has non-trivial recognition when at least two configurations are
  78distinguishable. At the primitive floor this is simply the existence of a
  79non-equality. -/
  80def NontrivialRecognition (K : Type*) : Prop :=
  81  ∃ x y : K, equalityDistinction K x y
  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) :