ConditionalSlot
plain-language theorem explainer
Packages an arbitrary proposition P as a type parameter with one field: a proof of P. Gravity and QG consumers cite it so contingent assumptions appear in every downstream type signature instead of hiding inside an always-inhabited witness shell. The declaration is a one-field structure (no proof body); the surrounding module proves it is inhabited exactly when P holds.
Claim. For any proposition $P$, a conditional slot of $P$ is a structure whose sole field is a proof that $P$ holds. Equivalently, the type is inhabited if and only if $P$ is true.
background
Scientist feedback flagged many gravity proofs as contingent on hidden definitions or hypotheses. The mechanical source is the old witness shell $W$ of shape $\Sigma(P:\mathrm{Prop}), P$: a structure carrying both a proposition field and a proof of it. That shell is always inhabited (take $P:=\top$), so at the type level "assumed nothing" and "assumed everything" are indistinguishable; consumers never see which $P$ was plugged in.
The Pattern-A fix lifts $P$ from an existential field to a type parameter. The resulting slot type makes $P$ part of every consumer signature: the trivial case is visibly True, and a hard convergence hypothesis is visibly that hypothesis. The compiler enforces the visibility a naming convention cannot.
This module sits in the Gravity domain and supplies both the target type and the formal justification for the lift, before a scripted repo-wide rewrite of master and sufficient-condition modules.
proof idea
No proof: this is a structure declaration with a single field holds : P. Inhabitation and emptiness are established by sibling lemmas, not here. Downstream, conditionalSlot_nonempty_iff is a two-direction constructor argument (project holds; pack a proof into the structure). The True and False special cases are one-line applications of that iff plus trivial / not_false.
why it matters
This is the target type of the Pattern-A lift on the quantum-gravity surface. Parent results in the same module use it directly: conditionalSlot_nonempty_iff (inhabited iff $P$), conditionalSlot_true_inhabited, conditionalSlot_false_not_inhabited (false assumptions become unconstructable), and the status bundle pattern_a_one_statement / patternALiftStatus.
The contrast with the vacuous shell is the point: false hypotheses can no longer be smuggled past type-checkers by instantiating an always-inhabited $\Sigma$-shell with $\top$. The type and its justification are landed; the remaining open step is the reviewed scripted transform (glm/pattern_a_conditionalslot_transform.py) that rewrites the large sufficient-conditions surface so every contingent gravity claim carries its assumptions in the signature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.