Gap4LedgerTerminalGuard
plain-language theorem explainer
Predicate recording the closed post-flip ledger state for gap-4 operator recovery: full-theory recovery bit true, campaign curved/QNM open bit cleared, and flat TT-axis convergence still marked proved on both the campaign and DiscreteLichnerowicz status records. Campaign auditors cite it as the terminal checklist after the R4∧R6 path. Pure four-way conjunction of status equalities; the sibling theorem discharges it by reflexivity.
Claim. The gap-4 ledger terminal guard is the proposition that the full-theory operator-recovery benchmark is set to true, the campaign curved/QNM open flag is false, the campaign records flat transverse-traceless convergence as proved, and the discrete Lichnerowicz status likewise records flat TT convergence as proved.
background
This module is the Wave C3 R0 decoy receipt for gap 4. The motivating residual is that the existing proposition "curved spectrum converges" is already inhabited by both scalar-coupling countermodels (coupling in ${1,2}$) while those operators disagree at every nonzero curvature. Inhabitation alone therefore must not flip the ledger terminal for curved discrete TT spectrum recovery.
Gap 4 in the seven-gaps campaign is discrete-to-continuum operator recovery. The Discrete Lichnerowicz status package states that flat 3-torus TT-axis convergence is proved (eigenvalue identity at every resolution, spectral limit $(2\pi k)^2$ on that sector), while curved background and QNM spectrum remain open. The full-theory benchmark record holds the global flip bit gap4_operator_recovery. The campaign status record tracks both the curved/QNM open bit and the flat TT proved bit.
The guard is the Prop that packages the intended closed configuration of those four bits.
proof idea
Not a proved theorem: a definitional Prop equal to the four-way conjunction of status-field equalities (full-theory gap-4 recovery true; campaign curved/QNM open false; campaign flat TT proved true; Discrete Lichnerowicz flat TT proved true). No tactics or lemmas. The downstream theorem of the same stem name inhabits the Prop by four rfl steps on those records.
why it matters
Gives the closed-guard checklist that the gap-4 ledger is supposed to satisfy after the R4∧R6 flip path: physical terminals inhabit the ledger, the curved/QNM open bit is cleared, and the flat-axis package remains. The parent theorem gap4LedgerTerminalGuard certifies the guard by reflexivity.
The surrounding module is deliberately a non-flip receipt. It composes banked blocker facts showing that curved-spectrum inhabitation is a decoy (countermodels at both couplings are not ledger-close), so the recovery benchmark must stay unflipped. Hard cores R2/R4/R6 remain open. In the broader RS gravity program this sits under discrete operator recovery toward continuum Lichnerowicz, not under the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.