W
plain-language theorem explainer
A witness shell is a dependent pair packing an arbitrary proposition with a proof of it. Its type is always inhabited (take True with the trivial proof), so any theorem that consumes such a shell is only as strong as the hidden proposition. Gravity and cost-algebra auditors cite it as the anti-pattern that made contingent lemmas look unconditional. It is a bare two-field structure with no proof obligations.
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 this witness shell: a structure whose fields are a proposition $P$ and a term of type $P$. As a type it is the dependent sum $\Sigma(P:\mathrm{Prop}),,P$, which is inhabited for every universe level by $\langle\mathrm{True},,\mathrm{trivial}\rangle$.
Consequently, at the type level "assumed nothing" and "assumed everything" are indistinguishable. A lemma that takes such a shell as a hypothesis can smuggle an arbitrarily strong $P$ without that $P$ showing up in the signature. The module ConditionalSlot records this defect and introduces the Pattern-A repair: lift $P$ from an existential field to a type parameter so every consumer's type mentions $P$ explicitly.
Local setting is pure type-theoretic hygiene for the gravity stack; no J-cost, phi-ladder, or continuum identification is used in the definition itself.
proof idea
No proof. The declaration is a two-field structure: a proposition field and a proof field of that proposition. Inhabitation and information content are established by sibling lemmas in the same module (the shell is always inhabited; the lifted slot is inhabited if and only if its parameter holds).
why it matters
This structure is the formal specimen of the contingency defect that motivated the whole ConditionalSlot module. Downstream, the module replaces it by a parameterized slot so that gravity and cost lemmas can no longer hide hypotheses behind an always-inhabited shell. The parent narrative is Pattern-A: make every assumed proposition a visible type parameter, so ConditionalSlot True is visibly trivial and ConditionalSlot HardConvergence is visibly that theorem.
In the broader Recognition stack this is scaffolding hygiene rather than a physics step: it does not touch T5–T8, the RCL, or the mass ladder. It does protect the audit trail for conditional gravity results that feed cost-algebra packaging (recognition cost systems with window length and reciprocal J-cost), where invisible hypotheses would otherwise make "proved" claims look stronger than they are. Name collisions with the window-length parameter $W$ in cost algebra are unrelated; this $W$ is only the vacuous witness shell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.