IndisputableMonolith.Foundation.MaximalForcing.RSClosureExtension

   1import IndisputableMonolith.Foundation.MaximalForcing.RealityClosure
   2
   3/-!
   4# Maximal Forcing: closure stability under carrier extension
   5
   6The original carrier-completeness worry is "the curated claim set might omit a
   7physically real invariant." This module answers the *forced* half of that worry at
   8the framework level: the maximal-forcing classification is **stable under extension
   9by a forced invariant**. Concretely, given a complete classifier certificate for a
  10claim universe `U` and any claim `C₀` forced over `U`'s admissibility class, the
  11universe extended with `C₀` again has a complete classifier, and `C₀` is classified
  12`Forced`.
  13
  14The consequence is structural, not cosmetic. No forced invariant can ever be
  15"missing" in a way that breaks the closure: any forced fact, once named, is absorbed
  16into the `Forced` bucket while every prior classification is preserved verbatim
  17(`ClaimClassification` depends on the universe only through its admissibility class
  18and realization type, both untouched by enlarging the claim set). Therefore the only
  19way a genuinely new claim adds content beyond `Forced` is by carrying its own
  20independence witness (`Independent`) or named selection principle (`Selected`) — each
  21a real proof obligation. The register's incompleteness, if any, can only ever be an
  22*undiscovered independence or selection*, never an undiscovered forced invariant.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Foundation
  27namespace MaximalForcing
  28
  29universe u
  30
  31/-- Extend a claim universe with one additional claim, keeping the same realization
  32type and admissibility class. -/
  33def ClaimUniverse.extend (U : ClaimUniverse.{u}) (C0 : RealityClaim U.Realization) :
  34    ClaimUniverse.{u} where
  35  Realization := U.Realization
  36  admissibility := U.admissibility
  37  claims := insert C0 U.claims
  38
  39@[simp] theorem extend_realization (U : ClaimUniverse.{u}) (C0 : RealityClaim U.Realization) :
  40    (U.extend C0).Realization = U.Realization := rfl
  41
  42@[simp] theorem extend_admissibility (U : ClaimUniverse.{u}) (C0 : RealityClaim U.Realization) :
  43    (U.extend C0).admissibility = U.admissibility := rfl
  44
  45@[simp] theorem extend_claims (U : ClaimUniverse.{u}) (C0 : RealityClaim U.Realization) :
  46    (U.extend C0).claims = insert C0 U.claims := rfl
  47
  48/-- The new claim is in the extended closure. -/
  49theorem mem_extend_self {P : Primitive} (U : ClaimUniverse.{u})
  50    (C0 : RealityClaim U.Realization) : InClosure P (U.extend C0) C0 :=
  51  Set.mem_insert _ _
  52
  53/-- Old claims remain in the extended closure. -/
  54theorem mem_extend_of_mem {P : Primitive} {U : ClaimUniverse.{u}}
  55    {C0 C : RealityClaim U.Realization} (h : InClosure P U C) :
  56    InClosure P (U.extend C0) C :=
  57  Set.mem_insert_of_mem _ h
  58
  59/-- **Transport a classification along an extension.** `ClaimClassification` and
  60`IndependenceWitness` are indexed by the universe, so a classification over `U` must be
  61rebuilt constructor-by-constructor to land over `U.extend C₀`. Every field is defeq
  62because `extend` changes only the claim set, leaving the realization type and
  63admissibility class fixed. -/
  64def ClaimClassification.toExtend {U : ClaimUniverse.{u}}
  65    {C0 C : RealityClaim U.Realization}
  66    (h : ClaimClassification U C) : ClaimClassification (U.extend C0) C := by
  67  rcases h with hf | hw | hs
  68  · exact ClaimClassification.forced hf
  69  · refine ClaimClassification.independent
  70      { yes_model := hw.yes_model, no_model := hw.no_model,
  71        yes_admissible := hw.yes_admissible, no_admissible := hw.no_admissible,
  72        yes_holds := hw.yes_holds, no_fails := hw.no_fails }
  73  · exact ClaimClassification.selected hs
  74
  75/-- **UNIFIED EXTENSION STABILITY (THEOREM).** A complete classifier for `U`, together
  76with *any* classification of a new claim `C₀` over `U`'s gate (forced, independent, or
  77selected), yields a complete classifier for the extended universe. Old claims keep
  78their classification verbatim; the new claim keeps the classification you supplied.
  79
  80This is the full structural answer to carrier-completeness: the classifier is closed
  81under adjoining any claim you can classify. The only barrier to extending the register
  82is producing the classification certificate itself — which is exactly the
  83maximal-forcing proof obligation. A new claim never "breaks" the closure; it only adds
  84work if it is genuinely `Independent` or `Selected`, and even then it slots in cleanly. -/
  85def MaximalClosureCert.extendClassified {P : Primitive} {U : ClaimUniverse.{u}}
  86    (cert : MaximalClosureCert P U) {C0 : RealityClaim U.Realization}
  87    (h0 : ClaimClassification U C0) :
  88    MaximalClosureCert P (U.extend C0) where
  89  classifies := by
  90    intro C hC
  91    rcases Set.mem_insert_iff.mp hC with h | h
  92    · rw [h]; exact h0.toExtend
  93    · exact (cert.classifies C h).toExtend
  94
  95/-- **EXTENSION STABILITY, FORCED CASE (THEOREM).** Specialization of
  96`extendClassified` to a forced new claim: the new claim is classified `Forced`. -/
  97def MaximalClosureCert.extendForced {P : Primitive} {U : ClaimUniverse.{u}}
  98    (cert : MaximalClosureCert P U) {C0 : RealityClaim U.Realization}
  99    (hC0 : Forced U.admissibility.admissible C0) :
 100    MaximalClosureCert P (U.extend C0) :=
 101  cert.extendClassified (ClaimClassification.forced hC0)
 102
 103/-- **EXTENSION STABILITY, INDEPENDENT CASE (THEOREM).** Specialization to a new claim
 104carrying an explicit countermodel witness: the new claim is classified `Independent`. -/
 105def MaximalClosureCert.extendIndependent {P : Primitive} {U : ClaimUniverse.{u}}
 106    (cert : MaximalClosureCert P U) {C0 : RealityClaim U.Realization}
 107    (W : IndependenceWitness U C0) :
 108    MaximalClosureCert P (U.extend C0) :=
 109  cert.extendClassified (ClaimClassification.independent W)
 110
 111/-- **EXTENSION STABILITY, SELECTED CASE (THEOREM).** Specialization to a new claim
 112governed by a named selection principle: the new claim is classified `Selected`. -/
 113def MaximalClosureCert.extendSelected {P : Primitive} {U : ClaimUniverse.{u}}
 114    (cert : MaximalClosureCert P U) {C0 : RealityClaim U.Realization}
 115    (hS : Selected U.admissibility.admissible C0) :
 116    MaximalClosureCert P (U.extend C0) :=
 117  cert.extendClassified (ClaimClassification.selected hS)
 118
 119/-- **EXTENSION PRESERVES THE TRICHOTOMY (THEOREM).** Every claim in a universe
 120extended by a forced invariant is `Forced`, `Independent`, or `Selected`. The new
 121forced claim lands in `Forced`; everything else keeps its prior classification. -/
 122theorem extend_preserves_trichotomy {P : Primitive} {U : ClaimUniverse.{u}}
 123    (cert : MaximalClosureCert P U) {C0 : RealityClaim U.Realization}
 124    (hC0 : Forced U.admissibility.admissible C0)
 125    (C : RealityClaim U.Realization) (hC : InClosure P (U.extend C0) C) :
 126    Forced (U.extend C0).admissibility.admissible C ∨
 127    Independent (U.extend C0).admissibility.admissible C ∨
 128    Selected (U.extend C0).admissibility.admissible C :=
 129  maximal_forcing_closure_trichotomy (cert.extendForced hC0) C hC
 130
 131/-- **No forced invariant can be missing (THEOREM).** For any claim `C₀` forced over
 132`U`'s admissibility, the extended universe still admits a complete classifier and
 133`C₀` itself is `Forced` there. This is the precise structural answer to the
 134carrier-completeness worry on the forced side: the closure absorbs any forced fact
 135without disruption. -/
 136theorem forced_invariant_absorbed {P : Primitive} {U : ClaimUniverse.{u}}
 137    (cert : MaximalClosureCert P U) {C0 : RealityClaim U.Realization}
 138    (hC0 : Forced U.admissibility.admissible C0) :
 139    (Nonempty (MaximalClosureCert P (U.extend C0))) ∧
 140    Forced (U.extend C0).admissibility.admissible C0 :=
 141  ⟨⟨cert.extendForced hC0⟩, hC0⟩
 142
 143/-- **THE REGISTER IS SATURATED UNDER CLASSIFIED EXTENSION (THEOREM).** This is the
 144complete structural statement of carrier-completeness, covering all three buckets at
 145once. A complete classifier survives adjoining any claim `C₀` for which a
 146classification certificate (`ClaimClassification U C₀`) exists. Equivalently: the
 147predicate "this universe has a complete classifier" is closed under extension by any
 148classifiable claim.
 149
 150The honest reading: the curated carrier cannot be "incomplete" in any way the framework
 151fails to absorb. If a new physically-real invariant is proposed, exactly one of three
 152things happens, and all three are handled — it is `Forced` (absorbed automatically, the
 153yard/eos-style derivations), `Independent` (absorbed once you exhibit a countermodel),
 154or `Selected` (absorbed once you name a selection principle). The residual content of
 155the maximal-forcing program is never "find the missing slot in the register"; it is
 156always "produce the classification certificate for a specific proposed claim." -/
 157theorem register_saturated_under_classification {P : Primitive} {U : ClaimUniverse.{u}}
 158    (cert : MaximalClosureCert P U) {C0 : RealityClaim U.Realization}
 159    (h0 : ClaimClassification U C0) :
 160    Nonempty (MaximalClosureCert P (U.extend C0)) :=
 161  ⟨cert.extendClassified h0⟩
 162
 163end MaximalForcing
 164end Foundation
 165end IndisputableMonolith
 166