ontology_summary

formal source

 316    - "Nothing" (x → 0⁺) has unbounded defect
 317    - Therefore only x = 1 is selected
 318    - Therefore existence is forced -/
 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) :=
 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) -/
 334theorem rs_true_or_of_left {C : Type*}
 335    {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
 336    {P Q : C → Bool} :
 337    RSTrue bridge B c₀ c_star P →
 338    RSTrue bridge B c₀ c_star (fun c => P c || Q c) := by
 339  intro ⟨hex, hval, N, hN⟩
 340  refine ⟨hex, by simp [hval], N, fun n hn => ?_⟩
 341  simp [hN n hn, hval]
 342
 343/-- RSTrue(Q) implies RSTrue(P ∨ Q). (Proposition 3.4, right case) -/
 344theorem rs_true_or_of_right {C : Type*}
 345    {bridge : CostBridge C} {B : C → C} {c₀ c_star : C}
 346    {P Q : C → Bool} :
 347    RSTrue bridge B c₀ c_star Q →
 348    RSTrue bridge B c₀ c_star (fun c => P c || Q c) := by
 349  intro ⟨hex, hval, N, hN⟩