gap4LedgerTerminalGuard
plain-language theorem explainer
The gap-4 ledger terminal guard holds: full-theory operator recovery is true, the campaign curved/QNM open bit is cleared, and both campaign and Discrete-Lichnerowicz flat TT-convergence flags are true. Campaign auditors cite it as the closed post-R4∧R6 ledger snapshot. The proof is a four-component reflexivity term on the banked Boolean constants.
Claim. The gap-4 ledger terminal guard holds: the full-theory benchmark flag for operator recovery equals $\mathrm{true}$, the campaign curved/QNM open bit equals $\mathrm{false}$, the campaign flat transverse-traceless convergence flag equals $\mathrm{true}$, and the Discrete-Lichnerowicz flat TT-convergence status equals $\mathrm{true}$.
background
Wave C3 residual R0 concerns whether inhabitation of the curved-spectrum convergence proposition alone can discharge the ledger terminal for discrete TT spectrum convergence on curved backgrounds. The module records that both scalar-coupling countermodels (coupling in ${1,2}$) already inhabit that proposition while disagreeing at every nonzero curvature, so inhabitation is a decoy and must not flip operator recovery by itself.
The closed guard packages the intended post-flip ledger state: physical terminals inhabit the full-theory benchmark, the campaign curved/QNM open bit is cleared, and the flat-axis package (campaign plus Discrete-Lichnerowicz) remains proved. Related holography ledger-closure predicates (even parity on a face or on both faces of a glued domino) are the same zero-sum bookkeeping idea at pixel scale; here the bookkeeping is campaign Boolean status rather than vertex bits.
Hard cores R2/R4/R6 stay open in this module. The receipt composes banked blocker facts and introduces no sorry, admit, or new axiom.
proof idea
Term-mode proof. The goal is the four-way conjunction defining the closed guard. Each conjunct is a Boolean equality against a concrete constant already present in the full-theory benchmark, the seven-gaps campaign status, or the Discrete-Lichnerowicz status record. The proof supplies the four equalities by rfl, i.e. definitional identity of those banked flags with the required values. No lemmas are rewritten; no case split or arithmetic is required.
why it matters
Sits in the Gravity SevenGaps campaign as the R0 decoy-receipt companion: it freezes the ledger snapshot that would hold after a legitimate R4∧R6 flip, while the surrounding module certifies that curved-spectrum inhabitation alone is not that flip. Downstream use list is empty in the graph; the declaration is a terminal status witness rather than a lemma consumed by a larger proof.
In the broader Recognition stack this is campaign hygiene, not a T0–T8 forcing step. It protects the discrete Lichnerowicz / flat TT axis already marked proved, and keeps the curved/QNM bit honest so gap-4 operator recovery cannot be claimed from decoy countermodels. Open work remains the hard cores R2/R4/R6 named in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.