conditionalSlot_nonempty_iff
plain-language theorem explainer
A conditional slot carrying a proof of proposition P is inhabited exactly when P holds. Gravity and foundation authors cite this when auditing Pattern-A lifts that make contingent hypotheses visible in type signatures. The proof is a two-direction constructor: unpack the holds field one way, pack a structure the other.
Claim. For every proposition $P$, the type of conditional slots that carry a proof of $P$ is nonempty if and only if $P$ is true.
background
The module formalizes the Pattern-A fix for contingent gravity proofs. The old witness shell is a dependent pair $\Sigma(P:\mathrm{Prop}), P$: it is always inhabited (by $\langle\mathrm{True},\mathrm{trivial}\rangle$), so a consumer theorem looks unconditional at the type level even when a hard hypothesis is plugged in.
The fix lifts the proposition from an existential field to a type parameter. A conditional slot for $P$ is the structure whose only field is a proof of $P$. Now $P$ appears in every consumer signature: a slot for $\mathrm{True}$ is visibly trivial; a slot for a hard convergence theorem is visibly that theorem.
This lemma is the information-content half of that justification: the lifted type carries exactly $P$, not more and not less.
proof idea
Term-mode iff by constructor. Left-to-right: given an inhabitant, project its holds field to recover $P$. Right-to-left: given a proof of $P$, pack the structure { holds := hp }. No external lemmas are required; the equivalence is definitional unpacking of the structure.
why it matters
This is item (2) in the module's stated goals: the lifted slot is inhabited iff its parameter holds. Downstream, conditionalSlot_false_not_inhabited rewrites through this equivalence to show a slot for $\mathrm{False}$ is unconstructable, the sharp contrast with the always-inhabited vacuous shell. The one-statement summary pattern_a_one_statement packages the same equivalence as the middle conjunct of the Pattern-A status report (target type landed; repo-wide lift still pending).
In the gravity stack this is infrastructure, not a physical law: it makes contingent assumptions (convergence hypotheses, hinge-mode conditions, and similar) compiler-visible so that "assumed nothing" and "assumed everything" stop being type-indistinguishable. It does not itself touch T0–T8, the RCL, or the mass ladder; it polices how those results may be consumed under named hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.