PatternALiftStatus
plain-language theorem explainer
Two-field status record for the Pattern-A lift on the quantum-gravity surface: whether the target conditional-slot type and its formal justification are landed, and whether the repo-wide scripted rewrite has been applied. Gravity auditors cite it to separate finished infrastructure from the pending cascade. Pure data structure; no proof content.
Claim. A status record with two Boolean flags: (i) the target conditional-slot type $P \mapsto \{h : P\}$ and its formal justification are in place; (ii) the repository-wide in-place lift across master and sufficient-condition modules has been applied.
background
The module answers a contingency raised in review: many proofs consumed a witness shell $W = \Sigma(P:\mathrm{Prop}),,P$, which is always inhabited (by $\langle\mathrm{True},\mathrm{trivial}\rangle$). At the type level, "assumed nothing" and "assumed everything" were indistinguishable, so contingent hypotheses hid inside existential fields.
The Pattern-A fix lifts the proposition to a type parameter: $\mathrm{ConditionalSlot}(P)$ is the type of proofs of $P$. Then $\mathrm{ConditionalSlot}(\mathrm{True})$ is visibly trivial and $\mathrm{ConditionalSlot}(H)$ for a hard hypothesis $H$ is visibly that hypothesis; the compiler enforces the visibility a naming convention cannot.
This structure is the bookkeeping object for how far that lift has progressed across the QG surface: target type plus justification on one flag, the gated 57k-line scripted cascade on the other.
proof idea
No proof. The declaration is a two-field structure of Booleans. Downstream, a concrete value sets the first flag true (target type and justification landed) and the second false (repo-wide lift still pending reviewed transform).
why it matters
Gives a single, machine-readable checkpoint for the Pattern-A migration that makes gravity contingencies honest in type signatures. The sole consumer is the concrete status value in this module, which records that the target type and formal justification are done while the repo-wide lift remains gated. That lift is the mechanical rewrite that would replace vacuous witness shells by parameterized conditional slots across master and sufficient-condition modules; until it lands, contingent gravity claims stay partially opaque. The structure itself does not touch T0–T8 or the RCL; it is process infrastructure for the QG surface so that later conditional gravity theorems can cite an explicit $P$ rather than a silent shell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.