pattern_a_one_statement
plain-language theorem explainer
Four facts in one package: the old witness shell is always inhabited (informationally empty); the lifted conditional slot is inhabited exactly when its proposition holds; the Pattern-A target type and justification are landed; the repo-wide mechanical lift is still pending. Gravity and foundation auditors cite it as the formal status certificate for the contingency fix. Proof is a four-component term pairing two prior lemmas with two definitional equalities.
Claim. The vacuous witness shell $\Sigma(P:\mathrm{Prop}),\,P$ is inhabited; for every proposition $P$, the conditional slot parameterized by $P$ is inhabited if and only if $P$ holds; the Pattern-A lift status records that the target type and its justification are landed, while the repository-wide lift has not been applied.
background
Scientist feedback flagged that many proofs were contingent on items that are definitions or hypotheses. The mechanical source is a witness shell of shape $\Sigma(P:\mathrm{Prop}),,P$: a proposition field together with a proof of that field. That shell is always inhabited (by $\langle\mathrm{True},\mathrm{trivial}\rangle$), so a theorem that consumes it is only as strong as the specific $P$ plugged in, and that $P$ is invisible in the type signature. At the type level, "assumed nothing" and "assumed everything" are indistinguishable.
The fix lifts $P$ from an existential field to a type parameter: a conditional slot for $P$ is simply a proof of $P$. Now $P$ appears in every consumer's signature. A slot for $\mathrm{True}$ is visibly trivial; a slot for a hard convergence theorem is visibly that theorem. The compiler enforces the visibility a naming convention cannot.
Upstream, the shell is proved always inhabited, and the slot is proved inhabited iff its parameter holds. The status record marks target-and-justification landed and repo-wide lift not yet applied.
proof idea
Term-mode packing of a four-way conjunction. First component: the prior lemma that the vacuous shell is always inhabited, witnessed by $\langle\mathrm{True},\mathrm{trivial}\rangle$. Second: the biconditional that the conditional slot type is nonempty exactly when its parameter holds (project the holds field one way; wrap a proof the other way). Third and fourth: reflexivity on the two boolean fields of the Pattern-A lift status record (target landed equals true; repo-wide lift equals false). No tactics beyond the term constructor.
why it matters
Single citation point for the Pattern-A fix status inside the gravity conditional-slot module. It closes the formal-justification half of the contingency problem: the old shell hides assumptions; the lifted slot makes them type-visible. Downstream gravity consumers that previously took opaque witness shells can be audited against these status flags. The repo-wide mechanical lift remains the open scripted step; this theorem records that gap explicitly rather than papering over it. No parent theorems currently depend on it, so it functions as a status certificate rather than a lemma in a longer forcing or gravity chain. It does not touch T0--T8, RCL, or the mass ladder; it is pure proof-hygiene infrastructure for the gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.