liftedTwoAssumption_nonempty_iff
plain-language theorem explainer
A two-parameter assumption shell is inhabited exactly when both propositions hold. Gravity and QG authors cite it to keep dual hypotheses visible in consumer types after the Pattern-A lift. The proof is a two-direction constructor: unpack the structure fields one way, pack them the other.
Claim. For any propositions $P_1$ and $P_2$, the type of pairs of proofs $(h_1:P_1,\, h_2:P_2)$ is inhabited if and only if $P_1 \land P_2$.
background
The ConditionalSlot module answers a contingency complaint: many RS gravity proofs consumed a witness shell W with a hidden field P : Prop and a proof of P. That shell is always inhabited (by ⟨True, trivial⟩), so at the type level "assumed nothing" and "assumed everything" look the same.
The fix lifts each assumption from an existential field to a type parameter. The one-parameter form is ConditionalSlot P with a single field holds : P. The two-parameter form used here is LiftedTwoAssumption P1 P2, a structure whose fields are proofs of P1 and P2 respectively; both propositions appear in every consumer signature.
This theorem is the two-assumption analogue of the one-parameter inhabitation equivalence already proved for ConditionalSlot: the lifted shell carries exactly the information of the conjunction, nothing more and nothing less.
proof idea
Bidirectional constructor on the ↔.
Left-to-right: from a term of Nonempty (LiftedTwoAssumption P1 P2), introduce the structure s and return the pair ⟨s.holds1, s.holds2⟩.
Right-to-left: from ⟨h1, h2⟩ : P1 ∧ P2, build the structure literal { holds1 := h1, holds2 := h2 } and wrap it in Nonempty.
No external lemmas; pure structure packing and unpacking.
why it matters
This is the formal justification that the Pattern-A two-assumption lift preserves content while making both hypotheses type-visible. The module doc lists it among the core claims: the old shell is always inhabited; the lifted form is inhabited iff its parameters hold.
Downstream gravity and discrete-QG developments that previously hid dual hypotheses (for example discrete Lichnerowicz sector assumptions, or paired continuum-limit and mode-sector hypotheses) can migrate to LiftedTwoAssumption without changing mathematical strength. The companion one-parameter results (conditionalSlot_nonempty_iff and friends) handle single hypotheses; this covers the common two-hypothesis case.
No parent theorems currently depend on it in the graph (used_by is empty); it is infrastructure for the migration status object that follows in the same file. It does not itself touch T0–T8, RCL, or the mass ladder; it is proof-engineering for the gravity surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.