`complete_godel_dissolution`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.GodelDissolution on GitHub at line 282.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.