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

ontology_summary

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)

 319theorem ontology_summary :
 320    (∀ x : ℝ, RSExists x ↔ x = 1) ∧
 321    (∃! x : ℝ, RSExists x) ∧
 322    (∃ ε > 0, ∀ x, 0 < x → x < ε → ¬RSExists x) ∧
 323    (∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x) :=

proof body

Term-mode proof.

 324  ⟨rs_exists_unique_one, rs_exists_unique, nothing_not_rs_exists, nothing_cannot_exist⟩
 325
 326/-! ## Disjunction Law for RSTrue (Paper Theorem 3.5 / Proposition 3.4)
 327
 328The paper proves that RSTrue distributes over disjunction:
 329- One direction (Proposition 3.4): RSTrue(P) ∨ RSTrue(Q) ⟹ RSTrue(P ∨ Q)
 330- Converse under RS-decidability (Theorem 3.5): RSTrue(P ∨ Q) ⟹ RSTrue(P) ∨ RSTrue(Q)
 331-/
 332
 333/-- RSTrue(P) implies RSTrue(P ∨ Q). (Proposition 3.4, left case) -/

depends on (10)

Lean names referenced from this declaration's body.