gap4OperatorDecoyReceiptStatus_flags
plain-language theorem explainer
Certifies the boolean snapshot of the Gap-4 operator-decoy receipt: decoy closed, physical-endomorphism and curved-spectrum terminals still open, QNM terminal not open, local recovery flag true, and the full-theory Gap-4 operator-recovery benchmark true. Gravity auditors tracking Seven-Gaps Wave C3 R0 cite it as the machine-checked receipt composition. Proof is a single decidability check on definitional booleans.
Claim. The Gap-4 operator-decoy receipt status has decoy receipt closed, physical endomorphism open, curved-spectrum terminal open, quasinormal-mode terminal not open, and Gap-4 operator recovery true; moreover the full-theory benchmark flag for Gap-4 operator recovery equals $\mathrm{true}$.
background
Wave C3 R0 packages a falsify-before-proving residual for Gap-4 operator recovery in the Seven Gaps gravity ledger. The existing proposition that the curved spectrum converges is already inhabited by both scalar-coupling countermodels (couplings in ${1,2}$), yet those operators disagree at every nonzero curvature. Mere inhabitation therefore does not discharge the ledger terminal for discrete curved TT-spectrum convergence and must not flip Gap-4 operator recovery.
The receipt status is a five-field boolean record: whether the decoy receipt is closed, whether the physical-endomorphism and curved-spectrum terminals remain open, whether the QNM terminal is open, and a local Gap-4 operator-recovery bit. The full-theory benchmarks structure holds campaign-level flags (bridge, continuum/measure, Lorentzian action, operator recovery, constraint recovery). Upstream, those benchmarks are the shared ledger state this certificate reads.
proof idea
One-line decidability proof. The tactic decide discharges the six boolean equalities by reducing against the definitional field values of the receipt-status structure and of the full-theory benchmarks record. No intermediate lemmas are applied.
why it matters
Terminal hygiene certificate for the Gap-4 operator-decoy receipt inside the Seven Gaps gravity campaign. It records that banked blocker facts (countermodel-inhabited curved-spectrum convergence that is not ledger-close) have been composed into a closed decoy receipt, while physical-endomorphism and curved-spectrum terminals stay open and hard cores R2/R4/R6 remain open. No downstream consumers are wired yet; the declaration is a status pin, not a lemma feeding further proofs. It does not advance the T0–T8 forcing chain; it polices false recovery of the discrete curved operator against the ledger terminal. Module brief: no sorry, admit, new axiom, or native_decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.