IndisputableMonolith.Foundation.MaximalForcing.ForcingClosure

   1import IndisputableMonolith.Foundation.MaximalForcing.AdmissibleRealization
   2
   3/-!
   4# Maximal Forcing: Closure Operator
   5
   6`ForcingClosure` is the claim set currently targeted by a primitive in a chosen
   7universe of realizations. The program is complete only when every claim in the
   8closure is classified as forced, independent, or selected with a named principle
   9that is itself scheduled for tightening.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace MaximalForcing
  15
  16universe u
  17
  18/-- A universe of realizations and claims for one maximal-forcing pass. -/
  19structure ClaimUniverse where
  20  Realization : Type u
  21  admissibility : AdmissibilityClass Realization
  22  claims : Set (RealityClaim Realization)
  23
  24/-- Closure operator: for a primitive and a claim universe, return the claims
  25whose status is being closed. Later phases will make this operator constructive
  26from syntax / semantics; here it is the execution interface. -/
  27def ForcingClosure (_P : Primitive) (U : ClaimUniverse.{u}) :
  28    Set (RealityClaim U.Realization) :=
  29  U.claims
  30
  31/-- A claim is in scope for maximal closure from a primitive. -/
  32def InClosure (P : Primitive) (U : ClaimUniverse.{u})
  33    (C : RealityClaim U.Realization) : Prop :=
  34  C ∈ ForcingClosure P U
  35
  36end MaximalForcing
  37end Foundation
  38end IndisputableMonolith
  39