TwoAssumptionShell
plain-language theorem explainer
Packages two arbitrary propositions together with proofs that each holds, the old master-theorem witness shape. Anyone auditing contingent gravity or master-theorem shells cites it as the two-hypothesis analogue of the single-field witness shell. As a structure definition it has no proof body; inhabitance is shown separately by plugging in True twice.
Claim. A two-assumption shell is a bundle of two propositions $P_1$ and $P_2$ together with certificates that $P_1$ holds and that $P_2$ holds. Equivalently, it is an element of $\Sigma(P_1:\mathrm{Prop}),\,P_1 \times \Sigma(P_2:\mathrm{Prop}),\,P_2$.
background
The ConditionalSlot module formalizes the Pattern-A fix for contingent proofs. Scientist feedback noted that many results rest on definitions or hypotheses that never appear in the consumer's type. The mechanical source is the single-field witness shell $W = \Sigma(P:\mathrm{Prop}),,P$, which is always inhabited by $\langle\mathrm{True},\mathrm{trivial}\rangle$, so "assumed nothing" and "assumed everything" are type-indistinguishable.
The two-assumption shell is the same pattern with two existential fields: two propositions and two holding certificates. Master-theorem style witnesses used this shape. Because both fields can be filled by True, the shell again carries no information at the type level.
The module's remedy is to lift each proposition from an existential field to a type parameter, yielding ConditionalSlot and its two-parameter analogue LiftedTwoAssumption. This declaration is the pre-lift object against which those fixes are measured.
proof idea
Pure structure definition: four fields (two Props and two proofs). No tactics, no lemmas. The companion theorem twoAssumptionShell_always_inhabited later exhibits a canonical inhabitant by setting both propositions to True with trivial proofs, confirming the shell is informationally vacuous at the type level.
why it matters
Anchors the "old shell is always inhabited" half of the Pattern-A justification in this module. The parent theorem twoAssumptionShell_always_inhabited cites it directly and shows Nonempty TwoAssumptionShell via True/True, so the shell "hides its content" exactly as the single-field W does. Downstream, LiftedTwoAssumption and liftedTwoAssumption_nonempty_iff replace both existential fields by type parameters, making contingency visible in every consumer signature. No physics constant or forcing-chain step (T0–T8) is claimed here; the declaration is scaffolding hygiene for gravity and master-theorem witnesses that previously buried hypotheses inside always-inhabited shells.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.