IndisputableMonolith.Foundation.GodelDissolution

   1import IndisputableMonolith.Foundation.BiconditionalSelfNegation
   2
   3/-!
   4# `GodelDissolution.lean` — Deprecated Backward-Compatibility Shim
   5
   6**This file is a deprecated alias.** The canonical content has moved to
   7`IndisputableMonolith.Foundation.BiconditionalSelfNegation`, with theorem
   8names that honestly describe what is proved.
   9
  10## Why the rename
  11
  12The Lean theorems formerly named `self_ref_query_impossible`,
  13`general_self_ref_impossible`, `godel_dissolution_holds`, and
  14`complete_godel_dissolution` prove a classical-logic triviality: no real
  15configuration `c` can satisfy `(defect c = 0) ↔ ¬(defect c = 0)`, because
  16that is `P ↔ ¬P` and has no model in any classical system. This fact is
  17correct, but it is unrelated to Gödel's first incompleteness theorem.
  18
  19A Gödel sentence is not `P ↔ ¬P`. It is `G ↔ ¬Prov_F(⌜G⌝)`, where `Prov_F`
  20is a syntactic provability predicate over Gödel numbers and `G` is a
  21sentence in the language of `F`. These are distinct propositions; the
  22biconditional is consistent (that is the whole point of Gödel I).
  23Treating a Gödel sentence as if it were `P ↔ ¬P` is a category error.
  24
  25The historical labeling was therefore misleading. The substantive
  26categorical argument that Gödel I has no target inside the RS forcing
  27chain (it targets recursively axiomatized proof systems for arithmetic
  28that maintain a syntactic `Prov` predicate separately from semantic
  29`True`; RS does not maintain that separation) is a meta-level argument,
  30not a Lean theorem. See `papers/Godel_And_RS_Closure_Honest_Assessment_20260520.html`
  31for the honest accounting.
  32
  33## Migration
  34
  35Replace imports of `IndisputableMonolith.Foundation.GodelDissolution`
  36with `IndisputableMonolith.Foundation.BiconditionalSelfNegation` at your
  37convenience. The old names below are preserved as aliases so existing
  38code continues to build.
  39
  40| Old name                            | New canonical name                                   |
  41|-------------------------------------|------------------------------------------------------|
  42| `GodelDissolution`                  | `BiconditionalSelfNegation`                          |
  43| `SelfRefQuery`                      | `SelfNegatingConfig`                                 |
  44| `GeneralSelfRefQuery`               | `GeneralSelfNegatingPredicate`                       |
  45| `self_ref_query_impossible`         | `no_self_negating_config`                            |
  46| `general_self_ref_impossible`       | `no_general_self_negating_predicate`                 |
  47| `self_ref_not_configuration`        | `no_self_negation_at_point`                          |
  48| `self_ref_not_rs_true`              | `self_negation_implies_false`                        |
  49| `GodelDissolutionTheorem`           | `ClassicalLogicAndUniqueMinimizerTheorem`            |
  50| `godel_dissolution_holds`           | `classical_logic_and_unique_minimizer_theorem`       |
  51| `complete_godel_dissolution`        | `complete_classical_logic_and_closure`               |
  52| `GodelRequirements`                 | `GodelTargetClassPrerequisites` (documentation only) |
  53| `RSDoesNotSatisfyGodel`             | `RsCategoricalDifferenceFromGodel` (documentation)   |
  54| `rs_avoids_godel`                   | `rs_categorical_difference_from_godel` (documentation)|
  55
  56The names `RSStab`, `RSDiverge`, `RSOutside`, `stab_decidable`,
  57`diverge_impossible`, `config_classification` are unchanged; they
  58accurately describe what they are.
  59-/
  60
  61namespace IndisputableMonolith
  62namespace Foundation
  63namespace GodelDissolution
  64
  65open Real
  66open LawOfExistence
  67open OntologyPredicates
  68
  69/-! Re-export the canonical new names from `BiconditionalSelfNegation`
  70into the legacy `GodelDissolution` namespace, so existing files that do
  71`open Foundation.GodelDissolution` can use the new honest names without
  72changing their `open` statements. -/
  73
  74export BiconditionalSelfNegation
  75  (SelfNegatingConfig GeneralSelfNegatingPredicate
  76   no_self_negating_config no_general_self_negating_predicate
  77   no_self_negation_at_point self_negation_implies_false
  78   ClassicalLogicAndUniqueMinimizerTheorem
  79   classical_logic_and_unique_minimizer_theorem
  80   complete_classical_logic_and_closure
  81   GodelTargetClassPrerequisites RsCategoricalDifferenceFromGodel
  82   rs_categorical_difference_from_godel)
  83
  84/-! ## Re-exported stabilization predicates -/
  85
  86/-- Re-export of `BiconditionalSelfNegation.RSStab`. -/
  87abbrev RSStab := BiconditionalSelfNegation.RSStab
  88
  89/-- Re-export of `BiconditionalSelfNegation.RSDiverge`. -/
  90abbrev RSDiverge := BiconditionalSelfNegation.RSDiverge
  91
  92/-- Re-export of `BiconditionalSelfNegation.RSOutside`. -/
  93abbrev RSOutside := BiconditionalSelfNegation.RSOutside
  94
  95/-- Re-export of `BiconditionalSelfNegation.stab_decidable`. -/
  96theorem stab_decidable (c : ℝ) : RSStab c ∨ ¬RSStab c :=
  97  BiconditionalSelfNegation.stab_decidable c
  98
  99/-- Re-export of `BiconditionalSelfNegation.diverge_impossible`. -/
 100theorem diverge_impossible (c : ℝ) : ¬RSDiverge c :=
 101  BiconditionalSelfNegation.diverge_impossible c
 102
 103/-- Re-export of `BiconditionalSelfNegation.config_classification`. -/
 104theorem config_classification (c : ℝ) : RSStab c ∨ RSOutside c :=
 105  BiconditionalSelfNegation.config_classification c
 106
 107/-! ## Re-exported structures (under deprecated names) -/
 108
 109/-- **Deprecated.** Renamed to `BiconditionalSelfNegation.SelfNegatingConfig`.
 110Despite the historical name, this is not a model of a Gödel sentence.
 111A Gödel sentence is `G ↔ ¬Prov(⌜G⌝)`, which is consistent. This structure
 112encodes `P ↔ ¬P`, which is uninhabited. -/
 113@[deprecated "Renamed to BiconditionalSelfNegation.SelfNegatingConfig" (since := "2026-05-20")]
 114abbrev SelfRefQuery := BiconditionalSelfNegation.SelfNegatingConfig
 115
 116/-- **Deprecated.** Renamed to `BiconditionalSelfNegation.GeneralSelfNegatingPredicate`. -/
 117@[deprecated "Renamed to BiconditionalSelfNegation.GeneralSelfNegatingPredicate"
 118  (since := "2026-05-20")]
 119abbrev GeneralSelfRefQuery := BiconditionalSelfNegation.GeneralSelfNegatingPredicate
 120
 121/-! ## Re-exported theorems (under deprecated names) -/
 122
 123set_option linter.deprecated false in
 124/-- **Deprecated.** Renamed to `BiconditionalSelfNegation.no_self_negating_config`.
 125Proves that no real configuration satisfies `(defect c = 0) ↔ ¬(defect c = 0)`.
 126This is a classical-logic triviality; it does not address Gödel sentences. -/
 127@[deprecated "Renamed to BiconditionalSelfNegation.no_self_negating_config"
 128  (since := "2026-05-20")]
 129theorem self_ref_query_impossible : ¬∃ q : SelfRefQuery, True :=
 130  BiconditionalSelfNegation.no_self_negating_config
 131
 132set_option linter.deprecated false in
 133/-- **Deprecated.** Renamed to
 134`BiconditionalSelfNegation.no_general_self_negating_predicate`. -/
 135@[deprecated "Renamed to BiconditionalSelfNegation.no_general_self_negating_predicate"
 136  (since := "2026-05-20")]
 137theorem general_self_ref_impossible : ¬∃ q : GeneralSelfRefQuery, True :=
 138  BiconditionalSelfNegation.no_general_self_negating_predicate
 139
 140/-- **Deprecated.** Renamed to `BiconditionalSelfNegation.no_self_negation_at_point`. -/
 141@[deprecated "Renamed to BiconditionalSelfNegation.no_self_negation_at_point"
 142  (since := "2026-05-20")]
 143theorem self_ref_not_configuration (c : ℝ) :
 144    ¬((defect c = 0) ↔ ¬(defect c = 0)) :=
 145  BiconditionalSelfNegation.no_self_negation_at_point c
 146
 147/-- **Deprecated.** Renamed to `BiconditionalSelfNegation.self_negation_implies_false`. -/
 148@[deprecated "Renamed to BiconditionalSelfNegation.self_negation_implies_false"
 149  (since := "2026-05-20")]
 150theorem self_ref_not_rs_true
 151    (c : ℝ)
 152    (h_encodes : ∀ P : Prop, (P ↔ RSStab c) → (P ↔ ¬RSStab c) → False)
 153    (h_correct : RSStab c ↔ ¬RSStab c) :
 154    False :=
 155  BiconditionalSelfNegation.self_negation_implies_false c h_encodes h_correct
 156
 157/-! ## Re-exported bundled theorem -/
 158
 159/-- **Deprecated.** Renamed to
 160`BiconditionalSelfNegation.ClassicalLogicAndUniqueMinimizerTheorem`. -/
 161@[deprecated "Renamed to BiconditionalSelfNegation.ClassicalLogicAndUniqueMinimizerTheorem"
 162  (since := "2026-05-20")]
 163abbrev GodelDissolutionTheorem :=
 164  BiconditionalSelfNegation.ClassicalLogicAndUniqueMinimizerTheorem
 165
 166set_option linter.deprecated false in
 167/-- **Deprecated.** Renamed to
 168`BiconditionalSelfNegation.classical_logic_and_unique_minimizer_theorem`. -/
 169@[deprecated "Renamed to BiconditionalSelfNegation.classical_logic_and_unique_minimizer_theorem"
 170  (since := "2026-05-20")]
 171theorem godel_dissolution_holds : GodelDissolutionTheorem :=
 172  BiconditionalSelfNegation.classical_logic_and_unique_minimizer_theorem
 173
 174set_option linter.deprecated false in
 175/-- **Deprecated.** Renamed to
 176`BiconditionalSelfNegation.complete_classical_logic_and_closure`. -/
 177@[deprecated "Renamed to BiconditionalSelfNegation.complete_classical_logic_and_closure"
 178  (since := "2026-05-20")]
 179theorem complete_godel_dissolution :
 180    (¬∃ q : SelfRefQuery, True) ∧
 181    (∃! x : ℝ, RSExists x) ∧
 182    (∀ x : ℝ, RSExists x ↔ x = 1) ∧
 183    (∀ c : ℝ, RSStab c ∨ ¬RSStab c) :=
 184  BiconditionalSelfNegation.complete_classical_logic_and_closure
 185
 186/-! ## Re-exported documentation-only structures -/
 187
 188/-- **Deprecated.** Renamed to
 189`BiconditionalSelfNegation.GodelTargetClassPrerequisites`.
 190Documentation record, not a theorem. -/
 191@[deprecated "Renamed to BiconditionalSelfNegation.GodelTargetClassPrerequisites"
 192  (since := "2026-05-20")]
 193abbrev GodelRequirements :=
 194  BiconditionalSelfNegation.GodelTargetClassPrerequisites
 195
 196/-- **Deprecated.** Renamed to
 197`BiconditionalSelfNegation.RsCategoricalDifferenceFromGodel`.
 198Documentation record, not a theorem. -/
 199@[deprecated "Renamed to BiconditionalSelfNegation.RsCategoricalDifferenceFromGodel"
 200  (since := "2026-05-20")]
 201abbrev RSDoesNotSatisfyGodel :=
 202  BiconditionalSelfNegation.RsCategoricalDifferenceFromGodel
 203
 204set_option linter.deprecated false in
 205/-- **Deprecated.** Renamed to
 206`BiconditionalSelfNegation.rs_categorical_difference_from_godel`.
 207Documentation-only `def`, not a theorem. -/
 208@[deprecated "Renamed to BiconditionalSelfNegation.rs_categorical_difference_from_godel"
 209  (since := "2026-05-20")]
 210def rs_avoids_godel : RSDoesNotSatisfyGodel :=
 211  BiconditionalSelfNegation.rs_categorical_difference_from_godel
 212
 213end GodelDissolution
 214end Foundation
 215end IndisputableMonolith
 216