gap4OperatorDecoyReceiptStatus
plain-language theorem explainer
Packages the Gap-4 operator decoy receipt as a fixed status record: R0 decoy closed, physical endomorphism and curved-spectrum terminals still open, QNM open-bit cleared, and the ledger recovery flag left true. Gravity campaign auditors cite it to freeze the falsify-before-proving residual that inhabitation of curved-spectrum convergence by both scalar couplings does not discharge the ledger terminal. It is a pure structure literal, not a proved theorem.
Claim. The Gap-4 operator decoy receipt status is the record with decoy receipt closed ($\mathrm{true}$), physical curved endomorphism open ($\mathrm{true}$), curved discrete TT-spectrum terminal open ($\mathrm{true}$), quasinormal-mode terminal open ($\mathrm{false}$), and Gap-4 operator-recovery ledger flag equal to $\mathrm{true}$.
background
Wave C3 residual R0 concerns the Gap-4 operator package in the Seven Gaps gravity campaign. The Prop that curved discrete TT spectra converge is already inhabited by both scalar-coupling countermodels (couplings in ${1,2}$), yet those operators disagree at every nonzero curvature. Inhabitation alone therefore does not discharge the ledger terminal that the curved discrete TT spectrum converges, and must not flip the Gap-4 operator-recovery flag.
The status structure is a five-bit receipt: R0 decoy closed; R2 physical curved endomorphism from Regge still open; R4 curved-spectrum ledger terminal still open; R6 QNM ledger terminal open-bit; and the unflipped recovery flag. A separate closed-guard Prop (after R4 and R6 flip) would require recovery true, campaign curved/QNM open cleared, and both campaign and Discrete Lichnerowicz flat TT-convergence proved.
Local setting: falsify-before-proving packaging of banked blocker theorems. No sorry, admit, new axiom, or native_decide.
proof idea
Definitional structure literal. Each field of the receipt status is assigned a concrete Bool: decoy closed true; physical endomorphism open true; curved-spectrum terminal open true; QNM terminal open false; operator recovery true. No lemmas, tactics, or computation; the value is the receipt itself.
why it matters
Freezes the R0 decoy fact so campaign ledgers cannot treat mere inhabitation of curved-spectrum convergence as Gap-4 recovery. Downstream, the flags theorem reads the five bits conjunctively and is the audit surface for this receipt.
In the Recognition gravity stack this sits under the Seven Gaps campaign: discrete Lichnerowicz flat TT work can proceed on the flat axis while curved operator underdetermination and full-theory ledger terminals stay honestly open. It does not advance T0–T8 forcing, RCL, or the phi-ladder mass formula; it is campaign hygiene for the curved-operator residual.
Hard cores R2 and R4 remain open on this receipt; the module states R2/R4/R6 stay open as research targets even though the QNM open-bit is recorded false here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.