IndisputableMonolith.Foundation.MaximalForcing.RealityClosure

   1import IndisputableMonolith.Foundation.MaximalForcing.ForcedInvariant
   2
   3/-!
   4# Maximal Forcing: Reality Closure Certificate
   5
   6This is the crown-theorem interface for the Maximal Forcing Closure program.
   7The final theorem is not asserted here. Instead, this module states the exact
   8certificate whose construction will be the theorem:
   9
  10```
  11forall C in ForcingClosure P U, ClaimClassification U C
  12```
  13
  14Once a real classifier is built for the final claim universe, the crown theorem
  15is a projection from that certificate.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace MaximalForcing
  21
  22universe u
  23
  24/-- A maximal closure certificate for a primitive and claim universe. -/
  25structure MaximalClosureCert (P : Primitive) (U : ClaimUniverse.{u}) where
  26  classifies :
  27    forall C : RealityClaim U.Realization,
  28      InClosure P U C -> ClaimClassification U C
  29
  30/-- Conditional crown theorem: once a classifier certificate exists, every claim
  31in the forcing closure is forced, independent, or selected. This is deliberately
  32conditional; the program is to build `MaximalClosureCert` for the real universe,
  33not to postulate it. -/
  34theorem maximal_forcing_closure
  35    {P : Primitive} {U : ClaimUniverse.{u}} (cert : MaximalClosureCert P U) :
  36    forall C : RealityClaim U.Realization,
  37      InClosure P U C -> ClaimClassification U C :=
  38  cert.classifies
  39
  40/-- Crown theorem in the exact disjunction form: given a classifier certificate,
  41every claim in the forcing closure is `Forced`, `Independent`, or `Selected`.
  42This is the literal "as forced as possible" statement; it concedes no contingency
  43lazily, because `Independent` and `Selected` are themselves proof obligations
  44(an explicit countermodel witness and a named selection principle, respectively).
  45-/
  46theorem maximal_forcing_closure_trichotomy
  47    {P : Primitive} {U : ClaimUniverse.{u}} (cert : MaximalClosureCert P U)
  48    (C : RealityClaim U.Realization) (hC : InClosure P U C) :
  49    Forced U.admissibility.admissible C ∨
  50    Independent U.admissibility.admissible C ∨
  51    Selected U.admissibility.admissible C := by
  52  rcases cert.classifies C hC with h | hw | hs
  53  · exact Or.inl h
  54  · exact Or.inr (Or.inl (independent_of_witness hw))
  55  · exact Or.inr (Or.inr hs)
  56
  57/-- Session protocol: closing a session on this program means either adding a
  58new forced invariant, adding an independence witness, tightening admissibility,
  59or updating the execution plan with the exact remaining blocker. -/
  60structure SessionUpdateProtocol where
  61  landed_forced_invariant : Prop
  62  landed_independence_witness : Prop
  63  tightened_admissibility : Prop
  64  updated_execution_plan : Prop
  65  nonempty_progress :
  66    landed_forced_invariant ∨
  67    landed_independence_witness ∨
  68    tightened_admissibility ∨
  69    updated_execution_plan
  70
  71end MaximalForcing
  72end Foundation
  73end IndisputableMonolith
  74