pith. machine review for the scientific record. sign in
theorem proved term proof

unification

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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. -/

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.