vacuousWitnessShell_always_inhabited
plain-language theorem explainer
The existential witness shell of shape Σ(P : Prop), P is always inhabited, via the trivial pair (True, proof of True). Auditors of contingent gravity or recognition proofs cite this to show why a bare shell type hides its assumptions at the signature level. The proof is a one-line term that builds that trivial inhabitant.
Claim. The type of pairs $(P, h)$ with $P$ a proposition and $h : P$ is nonempty: there exists at least one such pair (in particular $(True, \mathsf{trivial})$).
background
This module formalizes the Pattern-A fix for contingent proofs in the Recognition Science stack. Scientist feedback flagged that many results depend on definitions or hypotheses that never appear in the consumer's type. The mechanical source is the old witness shell: a structure with a field $P : \mathrm{Prop}$ and a proof that $P$ holds. As a type this is $\Sigma(P : \mathrm{Prop}),, P$.
Because the proposition is an existential field rather than a parameter, the shell type itself does not record which $P$ was intended. The module contrasts this with the lifted form $\mathrm{ConditionalSlot}(P)$, where $P$ is a type parameter and inhabitation is equivalent to $P$. The present theorem is the negative half of that contrast: the old shell is always inhabited, so its type carries no information about the assumption.
proof idea
Term-mode construction. Instantiate the shell with $P := \mathrm{True}$ and supply $\mathsf{trivial}$ as the proof of $\mathrm{True}$. The resulting pair is a closed inhabitant, so $\mathrm{Nonempty}$ of the shell type holds. No lemmas are needed beyond the structure constructor and the canonical proof of $\mathrm{True}$.
why it matters
This is item (1) in the module's formal justification of Pattern-A: the old shell always inhabited, hence information-free. Downstream, pattern_a_one_statement packages it with the positive half (lifted slot inhabited iff $P$) and the lift-status flags into a single conjunction. The sibling conditionalSlot_true_inhabited uses the contrast explicitly: $\mathrm{ConditionalSlot},\mathrm{True}$ is visibly trivial in the type, whereas a false assumption is unconstructable after the lift. The result is infrastructure for gravity and recognition proofs that must surface contingency rather than bury it in a $\Sigma$-shell. It does not itself force physical constants; it polices how contingent claims are typed before they enter the forcing chain or gravity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.