IndisputableMonolith.Foundation.MaximalForcing.AdmissibleRealization

   1import IndisputableMonolith.Foundation.MaximalForcing.Primitive
   2
   3/-!
   4# Maximal Forcing: Admissible Realization Classes
   5
   6Maximal forcing never concedes a degree of freedom lazily. If a claim is not
   7forced on the current admissible class, the next move is to either:
   8
   91. tighten admissibility by adding a deeper law that reality must satisfy; or
  102. prove independence by countermodel.
  11
  12This module defines the admissibility-class machinery used by the closure
  13operator.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace MaximalForcing
  19
  20universe u
  21
  22/-- A class of admissible realizations. The type `R` is deliberately abstract:
  23different phases may instantiate it with strict logic realizations, costed
  24realizations, physical models, or domain-specific structures. -/
  25structure AdmissibilityClass (R : Type u) where
  26  admissible : Set R
  27  label : String
  28
  29/-- Tightening from `A` to `B`: every `B`-admissible realization is
  30`A`-admissible. The optional strictness witness is a separate field so the core
  31order remains usable even when strictness is not yet known. -/
  32structure Tightening {R : Type u} (A B : AdmissibilityClass R) where
  33  subset : ∀ r : R, r ∈ B.admissible -> r ∈ A.admissible
  34  strict_witness : Prop
  35
  36/-- A claim forced after tightening is a target for promotion from `Selected` to
  37`Forced`. -/
  38def ForcedAfterTightening {R : Type u} (A B : AdmissibilityClass R)
  39    (C : RealityClaim R) : Prop :=
  40  Nonempty (Tightening A B) ∧ Forced B.admissible C
  41
  42/-- If a claim is forced on a wider admissible class, it remains forced after
  43tightening. -/
  44theorem forced_of_forced_under_tightening {R : Type u}
  45    {A B : AdmissibilityClass R} {C : RealityClaim R}
  46    (hT : Tightening A B) (hA : Forced A.admissible C) :
  47    Forced B.admissible C := by
  48  intro r hr
  49  exact hA r (hT.subset r hr)
  50
  51/-! ## Legitimacy of a tightening (Phase 5)
  52
  53The placeholder `strict_witness := True` carries no content. A tightening is
  54*legitimate* only if it does real work and is justified by a deeper law rather
  55than a free selection. The next definitions make legitimacy a proof obligation. -/
  56
  57/-- A tightening does real work when some realization admissible for the wider
  58class `A` is excluded by the narrower class `B`. This is derived from a genuine
  59independence-to-forcing flip: if a claim is independent over `A` but forced over
  60`B`, then the `A`-admissible realization that *fails* the claim cannot be
  61`B`-admissible, since everything `B`-admissible satisfies it. -/
  62theorem tightening_does_work {R : Type u} {A B : AdmissibilityClass R}
  63    {C : RealityClaim R}
  64    (hIndep : Independent A.admissible C) (hForced : Forced B.admissible C) :
  65    ∃ r : R, r ∈ A.admissible ∧ r ∉ B.admissible := by
  66  obtain ⟨_r0, r1, _h0, h1, _hC0, hnotC1⟩ := hIndep
  67  exact ⟨r1, h1, fun hr1B => hnotC1 (hForced r1 hr1B)⟩
  68
  69/-- A **legitimate** tightening. Beyond the subset order it carries:
  70
  71* `does_work`: a proof the gate is non-vacuous (some `A`-admissible realization is
  72  excluded by `B`); and
  73* `deeper_law` together with `deeper_law_proof`: the actual RS forcing theorem that
  74  justifies the added constraint, so the tightening is forced by a deeper law, not
  75  chosen freely. `deeper_law_label` names it for the audit.
  76
  77This replaces `strict_witness := True`: legitimacy is now a discharged proof
  78obligation, not a stored `True`. -/
  79structure LegitimateTightening {R : Type u} (A B : AdmissibilityClass R) where
  80  subset : ∀ r : R, r ∈ B.admissible -> r ∈ A.admissible
  81  does_work : ∃ r : R, r ∈ A.admissible ∧ r ∉ B.admissible
  82  deeper_law : Prop
  83  deeper_law_proof : deeper_law
  84  deeper_law_label : String
  85
  86/-- Every legitimate tightening is in particular a tightening (its stored
  87`strict_witness` is the deeper law it was justified by). -/
  88def LegitimateTightening.toTightening {R : Type u} {A B : AdmissibilityClass R}
  89    (L : LegitimateTightening A B) : Tightening A B where
  90  subset := L.subset
  91  strict_witness := L.deeper_law
  92
  93/-- Smart constructor. A genuine independence-to-forcing flip plus a named, proved
  94deeper law assembles a legitimate tightening. -/
  95def legitimateTightening_of_flip {R : Type u} {A B : AdmissibilityClass R}
  96    {C : RealityClaim R}
  97    (hsub : ∀ r : R, r ∈ B.admissible -> r ∈ A.admissible)
  98    (hIndep : Independent A.admissible C) (hForced : Forced B.admissible C)
  99    (law : Prop) (law_proof : law) (law_label : String) :
 100    LegitimateTightening A B where
 101  subset := hsub
 102  does_work := tightening_does_work hIndep hForced
 103  deeper_law := law
 104  deeper_law_proof := law_proof
 105  deeper_law_label := law_label
 106
 107end MaximalForcing
 108end Foundation
 109end IndisputableMonolith
 110