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

mp_physical

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)

 244theorem mp_physical :
 245    (∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x) ∧  -- Nothing is infinitely expensive
 246    (∃! x : ℝ, RSExists x) ∧  -- There exists exactly one existent thing
 247    (∀ x, RSExists x → x = 1)  -- That thing is unity
 248  := ⟨nothing_cannot_exist, rs_exists_unique, fun x hx => (rs_exists_unique_one x).mp hx⟩

proof body

Term-mode proof.

 249
 250/-- The Meta-Principle forces existence: since nothing is not selectable,
 251    something must be selected. -/

depends on (16)

Lean names referenced from this declaration's body.