LiftedTwoAssumption
plain-language theorem explainer
A two-parameter witness package that packages proofs of two propositions as fields, with both propositions visible as type parameters. Gravity and foundation consumers cite it when a result is contingent on a pair of named hypotheses rather than a single slot. There is no proof body: it is a pure structure definition whose content is exactly the pair of assumptions.
Claim. For propositions $P_1$ and $P_2$, the lifted two-assumption package is the type of pairs $(h_1, h_2)$ with $h_1 : P_1$ and $h_2 : P_2$. Both assumptions appear as parameters of the type, not as hidden existential fields.
background
The ConditionalSlot module formalizes the Pattern-A fix for contingent gravity proofs. The old witness shell was essentially $\Sigma(P:\mathrm{Prop}), P$: always inhabited (e.g. by $\langle\mathrm{True},\mathrm{trivial}\rangle$), so a consumer theorem looked unconditional while the real content of $P$ stayed invisible in the signature.
The fix lifts each assumption from an existential field to a type parameter. The one-parameter form is $\mathrm{ConditionalSlot}(P)$ with a single field $h:P$. The two-parameter form here does the same for a pair: both $P_1$ and $P_2$ sit in the type, so every downstream signature names exactly what is assumed.
Locally this is bookkeeping for gravity analysis (Regge/TT hinge and related zero-mode work), not a dynamical claim. The companion theorem states that the package is inhabited if and only if both propositions hold.
proof idea
No proof. The declaration is a structure with two fields: a proof of the first parameter and a proof of the second. Inhabitation and elimination are handled by the sibling biconditional (nonempty iff both hold), which constructs the structure from a conjunction and projects the two fields the other way.
why it matters
It is the two-hypothesis target type for the Pattern-A lift in this module. Downstream, the nonempty biconditional uses it to show that content is preserved while both assumptions stay visible in the type: inhabited exactly when $P_1\land P_2$.
That visibility is the point of the module: contingent gravity lemmas stop looking like unconditional theorems at the type level. Parent consumers can require an explicit package of two named hypotheses instead of a vacuous always-inhabited shell. It does not itself touch T0–T8, the RCL, or the mass ladder; it is infrastructure so those gravity claims can state their contingency honestly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.