IndisputableMonolith.Foundation.MaximalForcing.ForcedInvariant

   1import IndisputableMonolith.Foundation.MaximalForcing.IndependenceWitness
   2
   3/-!
   4# Maximal Forcing: Claim Classification
   5
   6Every claim in a closure target must eventually be classified as forced,
   7independent, or selected. `Selected` is an honest temporary tag, not an endpoint:
   8it must either be promoted to `Forced` by a deeper admissibility condition or
   9demoted to `Independent` by countermodel.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace MaximalForcing
  15
  16universe u
  17
  18/-- Classification of one claim in one closure universe. -/
  19inductive ClaimClassification (U : ClaimUniverse.{u})
  20    (C : RealityClaim U.Realization) : Prop where
  21  /-- Holds in every admissible realization. -/
  22  | forced : Forced U.admissibility.admissible C -> ClaimClassification U C
  23  /-- Two admissible realizations disagree on the claim. -/
  24  | independent : IndependenceWitness U C -> ClaimClassification U C
  25  /-- Not currently forced, but governed by a named selection principle. -/
  26  | selected : Selected U.admissibility.admissible C -> ClaimClassification U C
  27
  28/-- A forced invariant is a closure claim with a proof of forcedness. -/
  29structure ForcedInvariant (P : Primitive) (U : ClaimUniverse.{u}) where
  30  claim : RealityClaim U.Realization
  31  in_closure : InClosure P U claim
  32  forced : Forced U.admissibility.admissible claim
  33
  34end MaximalForcing
  35end Foundation
  36end IndisputableMonolith
  37