unification

formal source

 200composition law for the event space. When that hypothesis is supplied,
 201the recognizer's event space is a full Law-of-Logic carrier in the sense
 202of the rigidity paper. -/
 203theorem unification {𝒞 ℰ : Type*}
 204    (r : Recognizer 𝒞 ℰ) (weight : ℝ)
 205    (h : r.hasNontrivialRecognition) :
 206    -- Three definitional Aristotelian conditions:
 207    (∀ e : ℰ, r.cost weight e e = 0) ∧
 208    (∀ e₁ e₂ : ℰ, r.cost weight e₁ e₂ = r.cost weight e₂ e₁) ∧
 209    (∀ e₁ e₂ : ℰ, ∃ c : ℝ, r.cost weight e₁ e₂ = c) ∧
 210    -- Single-valuedness on unordered pairs (≡ Non-Contradiction):
 211    SingleValuedOnUnorderedPair (r.cost weight) ∧
 212    -- Primitive observer:
 213    (∃ (O : PrimitiveObserver ℰ) (e₁ e₂ : ℰ),
 214      e₁ ≠ e₂ ∧ Separates O e₁ e₂) := by
 215  refine ⟨?_, ?_, ?_, ?_, ?_⟩
 216  · exact Recognizer.identity r weight
 217  · exact Recognizer.non_contradiction r weight
 218  · exact Recognizer.totality r weight
 219  · exact Recognizer.singleValued r weight
 220  · exact Recognizer.induces_primitive_observer r h
 221
 222/-! ## Headline Certificate -/
 223
 224/-- **Recognizer-Induces-Logic Certificate.**
 225
 226The single forcing chain from Recognition Geometry to the Law of Logic
 227in its current form: the three definitional Aristotelian conditions are
 228automatic, the primitive observer is automatic, and the substantive
 229content reduces to a named compositional hypothesis. -/
 230structure RecognizerInducesLogicCert where
 231  identity_auto :
 232    ∀ {𝒞 ℰ : Type*} (r : Recognizer 𝒞 ℰ) (weight : ℝ),
 233      ∀ e : ℰ, r.cost weight e e = 0