twoAssumptionShell_always_inhabited
plain-language theorem explainer
The two-field witness shell (two propositions, each with a proof) is always inhabited: both fields can be True with trivial proofs. Auditors of master-theorem style gravity witnesses cite this to show the old shell carries no type-level content. The proof is a one-line inhabitant construction.
Claim. The type of pairs $(P_1, h_1, P_2, h_2)$ with $P_i : \mathrm{Prop}$ and $h_i : P_i$ is nonempty. Explicitly, it is inhabited by taking both propositions to be $\top$ with the trivial proofs.
background
This module formalizes the Pattern-A fix for contingent gravity witnesses. The mechanical problem is the old witness shell $W = \Sigma(P:\mathrm{Prop}), P$, which is always inhabited by $\langle \top, \mathrm{trivial}\rangle$. A theorem that consumes $W$ is only as strong as the hidden $P$; at the type level, "assumed nothing" and "assumed everything" look the same.
TwoAssumptionShell is the two-proposition variant used in master-theorem style witnesses: fields prop1, holds1, prop2, holds2. The lifted replacement is ConditionalSlot(P), where $P$ is a type parameter so every consumer's signature exposes the assumption. The module proves (1) old shells are always inhabited, and (2) the lifted slot is inhabited iff its parameter holds.
proof idea
Term-mode construction of an explicit inhabitant. Instantiate both proposition fields with True and both proof fields with trivial, then wrap in Nonempty.intro (angle-bracket syntax). No lemmas are required beyond the structure definition and the fact that $\top$ is provable.
why it matters
Closes item (1) of the module's stated program for the two-assumption case: the old shell "is also always inhabited (both props True), so it too hides its content." That fact is the formal justification for lifting master-theorem gravity witnesses from existential shells to ConditionalSlot-style parameters, so contingent hypotheses appear in type signatures rather than only in names.
No downstream consumers are wired yet (used_by is empty); the result is infrastructure for the Pattern-A audit of gravity claims, not a physics derivation. It does not touch T0–T8, RCL, or the mass ladder; it polices how those claims may be packaged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.