patternALiftStatus
plain-language theorem explainer
Records the current Pattern-A lift status on the quantum-gravity surface: the ConditionalSlot target type and its formal justification are in place, while the repo-wide scripted rewrite of master and sufficient-condition modules is still pending review. Gravity and verification authors cite it as the single source of truth for how far the contingency fix has progressed. The body is a two-field structure literal with boolean constants.
Claim. The Pattern-A lift status is the pair of booleans $(\mathsf{true},\mathsf{false})$: the target type $\mathsf{ConditionalSlot}(P)$ and its justification are landed, and the repo-wide in-place lift has not yet been applied.
background
Scientist feedback flagged that many gravity proofs were contingent on definitions or hypotheses hidden inside a witness shell
structure W where
P : Prop
holds : P
whose type is $\Sigma(P:\mathrm{Prop}),P$. That shell is always inhabited (by $\langle\mathrm{True},\mathrm{trivial}\rangle$), so a consumer theorem is only as strong as the plugged-in $P$, and $P$ never appears in the signature. "Assumed nothing" and "assumed everything" are type-indistinguishable.
Pattern A lifts $P$ to a type parameter:
structure ConditionalSlot (P : Prop) where
holds : P
Now every consumer signature exposes $P$. The status structure PatternALiftStatus tracks two booleans on the QG surface: whether that target type and its formal justification are landed, and whether the deterministic scripted transform has been applied across the master and sufficient-conditions modules (gated on review because it cascades through a large module).
proof idea
Definitional structure literal. The first field is set to true (target type and justification landed); the second to false (repo-wide lift not yet applied). No lemmas, no tactics.
why it matters
This is the live status flag for the Pattern-A contingency fix in the gravity stack. Downstream, pattern_a_one_statement packages four facts into one theorem: the old vacuous shell is always inhabited (carries no information); ConditionalSlot P is inhabited iff $P$; the target-and-justification bit is true; the repo-wide-lift bit is false. Citing this definition keeps that one-statement theorem honest about what is finished versus what remains a reviewed scripted transform. It does not itself touch T0–T8, RCL, or the mass ladder; it is infrastructure that makes conditional gravity claims type-visible rather than name-convention-visible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.