vacuousWitnessShell_inhabited_regardless
plain-language theorem explainer
Any true proposition Q yields two inhabited vacuous witness shells, one packing True and one packing Q. Auditors of contingent gravity lemmas cite this to show shell inhabitation carries no assumption content. The proof is a pure term that builds both shells side by side.
Claim. For every proposition $Q$ with a proof of $Q$, the type $\Sigma(P:\mathrm{Prop}),\,P$ (the vacuous witness shell) is nonempty in two ways at once: once with $P=\mathrm{True}$, and once with $P=Q$.
background
The module formalizes the Pattern-A fix for contingent proofs. Scientist feedback flagged that many gravity results quietly depend on definitions or hypotheses hidden inside a witness shell
structure W where
P : Prop
holds : P
whose type is $\Sigma(P:\mathrm{Prop}), P$. That shell is always inhabited (by $\langle\mathrm{True},\mathrm{trivial}\rangle$), so a consumer theorem is only as strong as the particular $P$ plugged in, and $P$ never appears in the type signature.
VacuousWitnessShell is exactly that anti-pattern structure: a proposition field plus a proof of it. The intended repair lifts $P$ to a type parameter (ConditionalSlot P), so contingency is visible to the compiler. This theorem is the contrast case: inhabitation of the old shell type reveals nothing about the assumption.
proof idea
Term-mode pair construction, no tactics. The left conjunct is the canonical trivial shell { P := True, holds := trivial }. The right conjunct reuses the given proof hQ as { P := Q, holds := hQ }. Both are wrapped in Nonempty via anonymous constructors, then paired. No lemmas are invoked; the argument is pure structure introduction.
why it matters
This is item (1) of the module's stated program: prove the old shell is always inhabited and therefore carries no information. Together with the sibling that the shell is inhabited even without any external hypothesis, it justifies replacing hidden $\Sigma$-shells by ConditionalSlot P throughout the gravity stack (Regge/TT analysis, seven-gap ledger work, posting-layer floors). Downstream consumers of contingent gravity claims need the type-level visibility this contrast motivates. No framework landmark (T0–T8, RCL, $\phi$-ladder) is proved here; the result is metatheoretic hygiene for those proofs. used_by is currently empty, so the declaration is justificatory rather than a production lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.