VacuousWitnessShell
plain-language theorem explainer
Defines the Pattern-A anti-pattern witness shell: a dependent pair packing an arbitrary proposition with a proof of it. Anyone auditing contingent gravity claims cites this as the type that hides assumptions in the signature. It is a bare structure definition (no proof obligation).
Claim. A witness shell is a pair $(P, h)$ where $P$ is a proposition and $h$ is a proof that $P$ holds; equivalently an element of $\Sigma(P:\mathrm{Prop}),\, P$.
background
Scientist feedback flagged many Recognition proofs as contingent on definitions or hypotheses that never appear in the consumer's type. The mechanical source is a witness shell of shape $\Sigma(P:\mathrm{Prop}),, P$: a structure carrying a field $P:\mathrm{Prop}$ and a field $\mathrm{holds}:P$.
Because the proposition is existentially quantified inside the type, the shell type itself does not expose which $P$ was used. Inhabitation of the shell therefore carries no information about the scientific assumption: the same type is inhabited whether $P$ is $\mathrm{True}$ or a deep unproved claim.
This module formalizes that diagnosis and the fix. The fix lifts $P$ to a type parameter (ConditionalSlot P), so every consumer signature names the contingency. The present declaration is the old, vacuous shell being diagnosed.
proof idea
No proof: this is a structure declaration with two fields, a proposition and a proof of that proposition. Downstream inhabitation lemmas construct concrete instances (e.g. $\langle\mathrm{True},,\mathrm{trivial}\rangle$) rather than deriving anything from this definition itself.
why it matters
This is the formal object whose vacuity motivates the Pattern-A lift across the gravity stack. Downstream, vacuousWitnessShell_always_inhabited shows the type is always nonempty, and vacuousWitnessShell_inhabited_regardless shows two shells with unrelated content are both inhabited, so inhabitation reveals nothing about the assumption.
Those facts feed pattern_a_one_statement, the module's one-line summary: the vacuous shell carries no information; the lifted conditional slot is inhabited iff its parameter holds; the target type and justification are landed; the repo-wide lift remains pending. Without naming this shell, the contingency critique stays informal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.