conditionalSlot_true_inhabited
plain-language theorem explainer
The conditional slot typed by True is inhabited: a witness exists whose only field is a proof of truth. Auditors of contingent gravity lemmas cite this as the positive half of the Pattern-A visibility fix. The proof is a one-line term that packages the trivial proof of True.
Claim. The type of conditional slots parameterized by $\top$ is nonempty: there exists a structure whose sole field is a proof of true.
background
Scientist feedback flagged that many gravity proofs look unconditional while silently consuming a witness shell
structure W where
P : Prop
holds : P
whose type is always inhabited by $\langle \top, \mathrm{trivial}\rangle$. At the type level, "assumed nothing" and "assumed a deep theorem" are indistinguishable.
The fix lifts the proposition from an existential field to a type parameter:
structure ConditionalSlot (P : Prop) where
holds : P
Now every consumer's signature displays $P$. The companion result vacuousWitnessShell_always_inhabited records that the old shell carries no information; this theorem records the trivial positive case of the lifted slot.
proof idea
One-line term proof. Construct the inhabitant as the structure whose holds field is trivial (the canonical proof of True). No lemmas are invoked; inhabitation of ConditionalSlot True is definitional.
why it matters
This is item (2) of the module's formal justification for the Pattern-A lift: the lifted slot is inhabited exactly when its parameter holds. Paired with the always-inhabited vacuous shell and with the negative companion (ConditionalSlot False is uninhabited), it makes contingency compiler-visible rather than naming-convention-visible.
No downstream consumers are wired yet (used_by is empty). The declaration is infrastructure for gravity modules that previously hid hypotheses inside witness shells (Regge/TT hinge analysis, seven-gap posting-layer floors, and related contingent lemmas). It does not itself touch T0–T8, RCL, or the mass ladder; it polices how those claims may be assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.