conditionalSlot_false_not_inhabited
plain-language theorem explainer
The conditional proof-slot for falsehood is empty: no term inhabits it. Auditors of Pattern-A gravity witnesses cite this to confirm a false assumption cannot be smuggled past the type checker. The proof rewrites via the slot-nonempty characterization and applies classical falsehood elimination.
Claim. The conditional slot for $\bot$ is uninhabited: $\neg\mathrm{Nonempty}(\mathrm{ConditionalSlot}(\bot))$. Equivalently, there is no package whose sole field is a proof of falsehood.
background
Scientist feedback flagged that many gravity proofs were contingent on definitions or hypotheses hidden inside witness shells. The old shell was a dependent pair $\Sigma(P:\mathrm{Prop}),,P$: a proposition field plus a proof of it. That type is always inhabited by $\langle\top,\mathrm{trivial}\rangle$, so at the type level "assumed nothing" and "assumed everything" look identical; the concrete $P$ never appears in consumer signatures.
The Pattern-A fix lifts $P$ from an existential field to a type parameter. The conditional slot is the structure with a single field holds : P. Now every consumer signature displays $P$ explicitly: the slot for $\top$ is visibly trivial, while the slot for a hard convergence statement is visibly that statement.
The companion theorem states that the slot is inhabited if and only if its parameter holds. That biconditional is the information-theoretic content of the lift, and is the sole upstream lemma this result needs.
proof idea
One-step rewrite. Apply the biconditional that the conditional slot for a proposition $P$ is nonempty precisely when $P$ holds, specializing to $P=\bot$. The goal reduces to $\neg\bot$, discharged by not_false. No case analysis or construction is required.
why it matters
This is the negative half of the Pattern-A justification in the ConditionalSlot module. Together with the positive half (the slot for $\top$ is inhabited) and the iff characterization, it proves the lifted type carries exactly the information of its parameter: true assumptions are constructible, false ones are not.
The contrast with the always-inhabited vacuous shell is the design point. Downstream migration examples in the same module (two-assumption shells shaped like master-theorem witnesses such as continuum-plus-Bianchi packages) rely on this visibility so that gravity contingency assumptions appear in every signature rather than being buried in a field. No parent theorem currently depends on this declaration by name; it is a local sanity check that closes the "false is unconstructable" side of the formal justification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.