IndisputableMonolith.Gravity.ConditionalSlot
Module cataloguing the Pattern-A witness-shell anti-pattern in conditional gravity packaging. A shell shaped like a dependent pair of a proposition with a proof of itself is always inhabited, so it cannot encode a real hypothesis. Auditors of RS gravity claims cite the inhabitedness lemmas to reject vacuous conditionals. Content is definitional plus elementary Nonempty arguments.
claimPattern A is the witness shell $\sum_{P:\mathrm{Prop}} P$. This type is always inhabited (witness $P=\top$), so inhabitation does not constrain any physical hypothesis. The module defines vacuous shells, conditional slots, two-assumption shells, and lifted two-assumption shells, and proves when each is nonempty: vacuous forms are always inhabited; genuine slots are nonempty iff the underlying proposition(s) hold.
background
In the Recognition Science gravity layer, conditional claims are sometimes wrapped as witness shells: dependent pairs that appear to bundle a hypothesis with evidence. Pattern A is the degenerate shell $\Sigma(P:\mathrm{Prop}),,P$. Choosing $P=\mathrm{True}$ always supplies an inhabitant, so the shell is nonempty independently of any gravity assumption under discussion.
The module lives in IndisputableMonolith.Gravity and imports only Mathlib. It introduces ConditionalSlot, VacuousWitnessShell, TwoAssumptionShell, and LiftedTwoAssumption, plus lemmas characterizing Nonempty for each. The setting is diagnostic hygiene: flag packaging that looks conditional but is vacuously true, before such shells are mistaken for genuine hypotheses on mass ladders, lensing, or galactic dynamics.
proof idea
Definition module with short inhabitedness proofs. VacuousWitnessShell is inhabited by the explicit witness $\langle\top,,\mathrm{True.intro}\rangle$, independently of any parameter. ConditionalSlot nonemptiness is an iff with the underlying proposition. Two-assumption and lifted variants get the same split: always-inhabited shells versus shells whose nonemptiness is equivalent to the conjunction of the named assumptions. No deep algebra; pure type inhabitation.
why it matters in Recognition Science
Conditional gravity results must not hide behind vacuously inhabited shells. This module names Pattern A so auditors can reject claims whose only evidence is a $\Sigma(P:\mathrm{Prop}),,P$ wrapper, and so authors avoid the anti-pattern when stating conditional slots. No downstream edges are recorded in the graph; the role is local Gravity-domain hygiene rather than a step in the T0–T8 forcing chain or the mass-ladder derivations. It supports clean separation between proved, conditional, and scaffolding gravity claims elsewhere in the monolith.
scope and limits
- Does not prove any physical gravity law or mass formula.
- Does not discharge real conditional hypotheses in the forcing chain.
- Does not connect to T0–T8, RCL, or phi-ladder numerics.
- Does not assert that every conditional slot in the repo is Pattern A.
- Does not provide a replacement pattern for genuine conditional claims.
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