IndisputableMonolith.Gravity.ConditionalSlot
Module isolating the Pattern-A anti-pattern in conditional gravity: witness shells of shape Σ(P:Prop), P, inhabited exactly when P holds. Gravity formalizers cite it when packaging assumptions as inhabited types rather than bare Props. Definitions plus elementary inhabitedness lemmas (vacuous shell always inhabited; conditional slot nonempty iff the proposition).
claimWitness shells of shape $\Sigma(P:\mathrm{Prop}),\,P$ (and two-assumption / lifted variants) are introduced, with characterizations: the vacuous shell is always inhabited; the conditional slot is inhabited if and only if the underlying proposition holds.
background
In Lean packaging of conditional physical claims, a hypothesis $P$ is sometimes wrapped as the dependent pair $\Sigma(P:\mathrm{Prop}),,P$. That type is inhabited precisely when $P$ is true. The module names this construction a Pattern-A witness shell (the anti-pattern of hiding a bare Prop behind a Sigma) and records the elementary inhabitedness facts.
Recognition Science gravity statements often sit behind named assumptions (profiles, screening, missing-mass hypotheses). Turning those assumptions into inhabited shells makes the conditional character visible in the type. The module isolates ConditionalSlot, VacuousWitnessShell, TwoAssumptionShell, and LiftedTwoAssumption so gravity files can reuse one packaging idiom.
proof idea
Definition module with elementary lemmas. Type constructors introduce the shells; inhabitedness proofs are direct Sigma introduction/elimination and Prop truth. Vacuous and two-assumption shells are always inhabited by construction; the conditional slot is nonempty iff its proposition holds; the lifted two-assumption form inherits the same equivalence.
why it matters in Recognition Science
Infrastructure for the Gravity domain: keeps conditional RS gravity claims honest about their hypothesis shells instead of burying Props in binder lists. Downstream gravity theorems that thread several assumptions through a single inhabited witness can import these shells. No parent theorems appear in the current dependency graph; the module is scaffolding for later conditional gravity results rather than a step on the T0-T8 forcing chain.
scope and limits
- Does not prove any physical gravity law or mass formula.
- Does not discharge the propositions packed inside the shells.
- Does not link to the forcing chain, RCL, or phi-ladder.
- Does not define numerical gravity observables or constants.
- Does not claim the shells are the only legitimate packaging of hypotheses.
declarations in this module (15)
-
structure
W -
structure
ConditionalSlot -
structure
VacuousWitnessShell -
theorem
vacuousWitnessShell_always_inhabited -
theorem
vacuousWitnessShell_inhabited_regardless -
theorem
conditionalSlot_nonempty_iff -
theorem
conditionalSlot_true_inhabited -
theorem
conditionalSlot_false_not_inhabited -
structure
TwoAssumptionShell -
theorem
twoAssumptionShell_always_inhabited -
structure
LiftedTwoAssumption -
theorem
liftedTwoAssumption_nonempty_iff -
structure
PatternALiftStatus -
def
patternALiftStatus -
theorem
pattern_a_one_statement