IndisputableMonolith.Foundation.MaximalForcing.IndependenceWitness

   1import IndisputableMonolith.Foundation.MaximalForcing.ForcingClosure
   2
   3/-!
   4# Maximal Forcing: Independence Witnesses
   5
   6If a claim is not forced, maximal closure demands a countermodel pair rather
   7than a vague appeal to contingency.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Foundation
  12namespace MaximalForcing
  13
  14universe u
  15
  16/-- Explicit countermodel pair for independence of a claim over an admissible
  17class. -/
  18structure IndependenceWitness (U : ClaimUniverse.{u})
  19    (C : RealityClaim U.Realization) where
  20  yes_model : U.Realization
  21  no_model : U.Realization
  22  yes_admissible : yes_model ∈ U.admissibility.admissible
  23  no_admissible : no_model ∈ U.admissibility.admissible
  24  yes_holds : C.holds yes_model
  25  no_fails : ¬ C.holds no_model
  26
  27/-- An explicit witness implies the proposition-level `Independent` tag. -/
  28theorem independent_of_witness {U : ClaimUniverse.{u}}
  29    {C : RealityClaim U.Realization}
  30    (W : IndependenceWitness U C) :
  31    Independent U.admissibility.admissible C := by
  32  exact ⟨W.yes_model, W.no_model, W.yes_admissible, W.no_admissible,
  33    W.yes_holds, W.no_fails⟩
  34
  35end MaximalForcing
  36end Foundation
  37end IndisputableMonolith
  38