IndisputableMonolith.Gravity.ConditionalSlot

   1import Mathlib
   2
   3/-!
   4# ConditionalSlot: the Pattern-A fix, formally justified
   5
   6## The contingency (scientist feedback)
   7
   8"a lot of the proofs are contingent on items that are definitions or hypotheses."
   9
  10The mechanical source is the witness shell
  11
  12```
  13structure W where
  14  P : Prop
  15  holds : P
  16```
  17
  18whose type is `Σ (P : Prop), P`. This shell is **always inhabited**
  19(by `⟨True, trivial⟩`), so a theorem that consumes it is only as strong as the
  20specific `P` plugged in -- and that `P` is invisible in the type signature. At
  21the type level "assumed nothing" and "assumed everything" are indistinguishable.
  22
  23## The fix
  24
  25Lift `P` from an existential field to a **type parameter**:
  26
  27```
  28structure ConditionalSlot (P : Prop) where
  29  holds : P
  30```
  31
  32Now `P` appears in every consumer's type signature. `ConditionalSlot True` is
  33visibly trivial; `ConditionalSlot HardConvergenceTheorem` is visibly that
  34theorem. The compiler enforces the visibility a naming convention cannot.
  35
  36## What this module proves
  37
  38This module is the formal justification for the Pattern-A lift, plus the target
  39type. It proves:
  40
  411. the old shell is **always inhabited** (carries no information);
  422. the lifted slot is inhabited **iff** its parameter holds (carries exactly the
  43   information of `P`);
  443. `ConditionalSlot False` is **not** inhabited (visible falsity);
  454. a two-field migration example (the `RegEHContinuumAndBianchi` shape) showing
  46   the lift preserves content while exposing both assumptions in the type.
  47
  48The repo-wide application of this lift across the master / sufficient-condition
  49modules is a deterministic scripted transform (see
  50`glm/pattern_a_conditionalslot_transform.py`), gated on review because it
  51cascades through the 57k-line `QuantumGravitySufficientConditions.lean`.
  52
  53Status: THEOREM. Zero `sorry`, zero `axiom`.
  54-/
  55
  56namespace IndisputableMonolith
  57namespace Gravity
  58namespace ConditionalSlot
  59
  60/-! ## §1. The old vacuous shell carries no information -/
  61
  62/-- The Pattern-A anti-pattern: a witness shell of shape `Σ (P : Prop), P`. -/
  63structure VacuousWitnessShell where
  64  P : Prop
  65  holds : P
  66
  67/-- **The shell is always inhabited**, by `⟨True, trivial⟩`. Hence its type
  68carries no information about what was assumed: every such shell can be
  69constructed, whether the intended `P` is a deep theorem or `True`. This is
  70exactly why a "theorem" consuming a shell hides its contingency. -/
  71theorem vacuousWitnessShell_always_inhabited : Nonempty VacuousWitnessShell :=
  72  ⟨{ P := True, holds := trivial }⟩
  73
  74/-- Two shells with completely different content are nonetheless both inhabited,
  75witnessing that inhabitation of the shell type tells you nothing about the
  76assumption. -/
  77theorem vacuousWitnessShell_inhabited_regardless (Q : Prop) (hQ : Q) :
  78    Nonempty VacuousWitnessShell ∧ Nonempty VacuousWitnessShell :=
  79  ⟨⟨{ P := True, holds := trivial }⟩, ⟨{ P := Q, holds := hQ }⟩⟩
  80
  81/-! ## §2. The lifted slot exposes its assumption -/
  82
  83/-- The Pattern-A fix: the proposition is a **type parameter**, not a hidden
  84existential field. The assumption `P` now appears in the type. -/
  85structure ConditionalSlot (P : Prop) where
  86  holds : P
  87
  88/-- **The slot is inhabited iff its parameter holds.** Unlike the vacuous shell,
  89the slot type carries exactly the information of `P`: you can build it precisely
  90when `P` is true. -/
  91theorem conditionalSlot_nonempty_iff (P : Prop) :
  92    Nonempty (ConditionalSlot P) ↔ P := by
  93  constructor
  94  · rintro ⟨s⟩; exact s.holds
  95  · intro hp; exact ⟨{ holds := hp }⟩
  96
  97/-- `ConditionalSlot True` is trivially inhabited -- and visibly so, because the
  98parameter is `True` right there in the type. -/
  99theorem conditionalSlot_true_inhabited : Nonempty (ConditionalSlot True) :=
 100  ⟨{ holds := trivial }⟩
 101
 102/-- `ConditionalSlot False` is **not** inhabited. The contrast with
 103`vacuousWitnessShell_always_inhabited` is the whole point: a false assumption is
 104now visibly unconstructable, whereas the vacuous shell would have been
 105constructed anyway with `P := True`. -/
 106theorem conditionalSlot_false_not_inhabited : ¬ Nonempty (ConditionalSlot False) := by
 107  rw [conditionalSlot_nonempty_iff]
 108  exact not_false
 109
 110/-- Recover the carried proof from a slot. -/
 111theorem ConditionalSlot.proof {P : Prop} (s : ConditionalSlot P) : P := s.holds
 112
 113/-! ## §3. Migration example: a two-assumption shell
 114
 115The master-theorem witnesses have shapes like `RegEHContinuumAndBianchi`, which
 116carry two `Prop` fields each. We show the lift on that shape: both assumptions
 117become type parameters, visible in every signature, with content preserved. -/
 118
 119/-- The old two-assumption shell shape (as in the master-theorem witnesses). -/
 120structure TwoAssumptionShell where
 121  prop1 : Prop
 122  holds1 : prop1
 123  prop2 : Prop
 124  holds2 : prop2
 125
 126/-- The old two-assumption shell is also always inhabited (both props `True`),
 127so it too hides its content. -/
 128theorem twoAssumptionShell_always_inhabited : Nonempty TwoAssumptionShell :=
 129  ⟨{ prop1 := True, holds1 := trivial, prop2 := True, holds2 := trivial }⟩
 130
 131/-- The lifted two-assumption form: both propositions are parameters. -/
 132structure LiftedTwoAssumption (P1 P2 : Prop) where
 133  holds1 : P1
 134  holds2 : P2
 135
 136/-- The lifted form is inhabited iff both assumptions hold -- content preserved,
 137both assumptions now visible in the type. -/
 138theorem liftedTwoAssumption_nonempty_iff (P1 P2 : Prop) :
 139    Nonempty (LiftedTwoAssumption P1 P2) ↔ (P1 ∧ P2) := by
 140  constructor
 141  · rintro ⟨s⟩; exact ⟨s.holds1, s.holds2⟩
 142  · rintro ⟨h1, h2⟩; exact ⟨{ holds1 := h1, holds2 := h2 }⟩
 143
 144/-! ## §4. The migration status object -/
 145
 146/-- Status of the Pattern-A lift across the QG surface. -/
 147structure PatternALiftStatus where
 148  /-- The target `ConditionalSlot` type and its justification are in place. -/
 149  target_type_and_justification_landed : Bool
 150  /-- The repo-wide in-place lift across master / sufficient-condition modules
 151  has been applied. (A deterministic scripted transform; cascades through the
 152  57k-line sufficient-conditions module, so it is gated on review.) -/
 153  repo_wide_lift_applied : Bool
 154
 155/-- Current Pattern-A status: the target type and its formal justification are
 156landed; the repo-wide lift is pending the reviewed scripted transform. -/
 157def patternALiftStatus : PatternALiftStatus where
 158  target_type_and_justification_landed := true
 159  repo_wide_lift_applied := false
 160
 161/-- **One-statement.** The vacuous shell carries no information (always
 162inhabited); the lifted `ConditionalSlot` carries exactly its parameter
 163(inhabited iff `P`); the target and justification are landed; the repo-wide lift
 164remains the pending scripted step. -/
 165theorem pattern_a_one_statement :
 166    Nonempty VacuousWitnessShell ∧
 167    (∀ P : Prop, Nonempty (ConditionalSlot P) ↔ P) ∧
 168    patternALiftStatus.target_type_and_justification_landed = true ∧
 169    patternALiftStatus.repo_wide_lift_applied = false :=
 170  ⟨vacuousWitnessShell_always_inhabited, conditionalSlot_nonempty_iff, rfl, rfl⟩
 171
 172end ConditionalSlot
 173end Gravity
 174end IndisputableMonolith
 175