`complete_godel_dissolution`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.GodelDissolution
domain: Foundation
line: 282 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.GodelDissolution on GitHub at line 282.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 279    Closure in RS means "unique J-minimizer exists."
 280    Gödel says "consistent systems can't prove all arithmetic."
 281    These don't conflict. -/
 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) :=
 291  ⟨self_ref_query_impossible, rs_exists_unique, rs_exists_unique_one, stab_decidable⟩
 292
 293end GodelDissolution
 294end Foundation
 295end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.