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

complete_godel_dissolution

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)

 282theorem complete_godel_dissolution :
 283    -- Self-ref queries impossible
 284    (¬∃ q : SelfRefQuery, True) ∧
 285    -- Unique RS-existent
 286    (∃! x : ℝ, RSExists x) ∧
 287    -- That existent is unity
 288    (∀ x : ℝ, RSExists x ↔ x = 1) ∧
 289    -- Every config has definite status
 290    (∀ c : ℝ, RSStab c ∨ ¬RSStab c) :=

proof body

Term-mode proof.

 291  ⟨self_ref_query_impossible, rs_exists_unique, rs_exists_unique_one, stab_decidable⟩
 292
 293end GodelDissolution
 294end Foundation
 295end IndisputableMonolith

depends on (16)

Lean names referenced from this declaration's body.