kernel_symm

formal source

  56    I.kernel x x := rfl
  57
  58/-- The observer kernel is symmetric. -/
  59theorem kernel_symm {K : Type*} (I : PrimitiveInterface K) {x y : K}
  60    (h : I.kernel x y) : I.kernel y x := h.symm
  61
  62/-- The observer kernel is transitive. -/
  63theorem kernel_trans {K : Type*} (I : PrimitiveInterface K) {x y z : K}
  64    (hxy : I.kernel x y) (hyz : I.kernel y z) : I.kernel x z :=
  65  hxy.trans hyz
  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