Recognizer

proof body

Definition body.

  74  r.observe x = r.observe y
  75
  76/-- The kernel of a recognizer is an equivalence relation. -/
  77theorem Recognizer.kernel_is_equivalence {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ) :
  78    Equivalence (r.kernel) :=
  79  ⟨fun _ => rfl, fun h => h.symm, fun h₁ h₂ => h₁.trans h₂⟩
  80
  81/-! ## The Recognizer-Induced Cost on the Event Space -/
  82
  83/-- The cost of distinguishing two events: zero when they are the same
  84event, a positive weight otherwise. This is exactly the equality-induced
  85cost of `PrimitiveDistinction` applied to the event space `ℰ`. -/
  86noncomputable def Recognizer.cost {𝒞 ℰ : Type*} (_r : Recognizer 𝒞 ℰ)
  87    (weight : ℝ) : ℰ → ℰ → ℝ :=
  88  equalityCost ℰ weight
  89
  90/-! ## The Three Definitional Aristotelian Conditions
  91
  92A recognizer induces (L1), (L2), and (L3a) on its event space
  93automatically, by `PrimitiveDistinction`. No further structural choice
  94is required.
  95-/
  96
  97/-- **(L1) Identity from the recognizer.** The cost of distinguishing an
  98event from itself is zero. -/
  99theorem Recognizer.identity {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ)
 100    (weight : ℝ) :
 101    ∀ e : ℰ, r.cost weight e e = 0 := by
 102  intro e
 103  exact identity_from_equality ℰ weight e
 104
 105/-- **(L2) Non-Contradiction from the recognizer.** The cost of
 106distinguishing `e₁` from `e₂` equals the cost of distinguishing `e₂`
 107from `e₁`. -/
 108theorem Recognizer.non_contradiction {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ)
 109    (weight : ℝ) :
 110    ∀ e₁ e₂ : ℰ, r.cost weight e₁ e₂ = r.cost weight e₂ e₁ := by
 111  intro e₁ e₂
 112  exact non_contradiction_from_equality ℰ weight e₁ e₂
 113
 114/-- **(L3a) Totality from the recognizer.** The cost is defined and
 115returns a value for every pair of events. -/
 116theorem Recognizer.totality {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ)
 117    (weight : ℝ) :
 118    ∀ e₁ e₂ : ℰ, ∃ c : ℝ, r.cost weight e₁ e₂ = c := by
 119  intro e₁ e₂
 120  exact totality_from_function_type ℰ weight e₁ e₂
 121
 122/-- **Single-valuedness from the recognizer.** The induced cost is a
 123single-valued function on unordered pairs of events; equivalently, by
 124`MagnitudeOfMismatch`, it is symmetric. -/
 125theorem Recognizer.singleValued {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ)
 126    (weight : ℝ) :
 127    SingleValuedOnUnorderedPair (r.cost weight) :=
 128  equalityCost_singleValued ℰ weight
 129
 130/-! ## The Primitive Observer is the Recognizer
 131
 132Once the event space has at least two distinct events, the recognizer
 133delivers the primitive observer of `ObserverFromRecognition`. This is the
 134unification: the recognizer of Recognition Geometry **is** the primitive
 135observer of the Law-of-Logic chain. They are the same object.
 136-/
 137
 138/-- The event space of a recognizer admits non-trivial recognition iff
 139it contains at least two distinct events. -/
 140def Recognizer.hasNontrivialRecognition {𝒞 ℰ : Type*}
 141    (_r : Recognizer 𝒞 ℰ) : Prop :=
 142  ∃ e₁ e₂ : ℰ, e₁ ≠ e₂
 143
 144/-- **Recognizer is observer.** Any recognizer with a non-trivially
 145populated event space induces a primitive observer (a finite-valued
 146interface) that separates two distinct events.
 147
 148This is the unification: the geometric primitive (recognizer producing
 149event space) and the logical primitive (interface producing primitive
 150observer) are the same act. -/
 151theorem Recognizer.induces_primitive_observer {𝒞 ℰ : Type*}
 152    (r : Recognizer 𝒞 ℰ) (h : r.hasNontrivialRecognition) :
 153    ∃ (O : PrimitiveObserver ℰ) (e₁ e₂ : ℰ),
 154-- ... 50 more lines elided ...