Gap4OperatorDecoyReceiptStatus
plain-language theorem explainer
Five-field Boolean status record for Gap-4 operator recovery after the R0 decoy receipt: decoy closed, physical curved endomorphism open, curved TT-spectrum terminal open, QNM terminal open/closed bit, and the unflipped recovery flag. Gravity campaign auditors cite it as the typed snapshot of what the decoy package certifies without flipping ledger terminals. It is a plain structure definition; the inhabited witness is the sibling value that fills the bits.
Claim. A status record with five Boolean fields: (i) whether the R0 decoy receipt is closed; (ii) whether the physical curved endomorphism from Regge remains open; (iii) whether the ledger terminal for discrete TT-spectrum convergence on curved backgrounds remains open; (iv) whether the quasinormal-mode spectrum ledger terminal remains open; (v) whether the gap-4 operator-recovery ledger flag is still unflipped.
background
Wave C3 residual R0 packages a falsify-before-proving fact about Gap-4 operator recovery in the seven-gaps gravity campaign. The Prop that curved discrete 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 for curved TT-spectrum convergence and must not flip the gap-4 operator-recovery flag.
A ledger here is a double-entry collection of recognition events (or quantum-ledger entries with conserved log-ratio balance). Downstream campaign and full-theory ledgers expose Boolean terminals for curved spectrum convergence, quasinormal modes, and operator recovery. The sibling closed guard after a genuine R4$\land$R6 flip would require recovery true, curved/QNM open bit cleared, and the flat TT-convergence package proved on both campaign and Discrete Lichnerowicz status.
This module only records the R0 decoy receipt composition. Hard cores R2 (physical curved endomorphism from Regge), R4 (curved spectrum terminal), and R6 (QNM terminal) stay open; no flag flips.
proof idea
No proof body: the declaration is a structure (record type) with five named Bool fields and field doc-comments fixing the intended semantics (R0 decoy closed; R2/R4/R6 open bits; recovery unflipped). Instantiation is deferred to the sibling value that assigns concrete bits. No tactics, lemmas, or algebraic reduction.
why it matters
Gives the typed carrier for the R0 decoy-receipt snapshot in the Gap-4 residual DAG. The sole direct consumer is the sibling witness that sets decoy closed, physical endomorphism open, curved-spectrum terminal open, and records the recovery/QNM bits without claiming a flip.
In the Recognition gravity stack this blocks a false positive: countermodel inhabitation of curved-spectrum convergence must not be read as ledger discharge of discrete_tt_spectrum_converges_curved or as operator recovery. That keeps the campaign honest relative to the flat-axis Discrete Lichnerowicz package and the closed-guard Prop that would only hold after genuine R4$\land$R6 closure.
It does not advance T5–T8 forcing, RCL, or the mass ladder; it is campaign hygiene on the gravity residual side so later curved/QNM work cannot silently promote a decoy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.