gap6LedgerTerminalGuard
plain-language theorem explainer
After Gap 6 closed via the V2 Wick action continuation, five ledger status bits sit in a fixed terminal pattern: full-theory Lorentzian action true, campaign and 4D causal-simplex action-open flags cleared, kinematical Wick certified, 3D Lorentzian-sector action still open. The lookalike-decoy residual package cites this guard as the post-close witness. Proof is five definitional equalities.
Claim. The Gap-6 ledger terminal guard holds: the full-theory benchmark for Lorentzian action equals true, the campaign flag that Gap-6 action continuation is open equals false, the 4D causal-simplex flag that action-level continuation is open equals false, the Lorentzian-sector flag that Lorentzian action continuation is open equals true, and the campaign flag that Gap-6 kinematical Wick is certified equals true.
background
Module setting is Wave C4 R0: a lookalike-falsify receipt for Gap 6 in the Seven Gaps gravity campaign. Gap 6 is the Lorentzian / Wick action-continuation obligation. F3 succession closed it by wick_action_continuation_4d_v2; lookalike mathematics is retained only as separation certificates so that later sessions cannot rename a weaker object into the ledger terminal.
The guard proposition packages five boolean ledger fields after that close: full-theory Gap-6 Lorentzian action flipped on; campaign and CausalSimplex4D action-open bits cleared; kinematical Wick certified; the 3D LorentzianSector action-continuation bit deliberately left open. Doc-comment: "Gap6 flipped via V2; campaign / CausalSimplex4D action-open bits cleared; kinematical Wick certified; 3D LorentzianSector action bit remains open."
Upstream status structures (fullTheoryBenchmarks, sevenGapsCampaignStatus, causalSimplex4DStatus, lorentzianSectorStatus) are the campaign ledger; this theorem only asserts their post-F3 values, not the analytic content of the Wick continuation itself.
proof idea
Term-mode constructor proof: the goal is a five-fold conjunction of boolean equalities, and each conjunct is definitionally true against the current ledger constants. The proof is therefore ⟨rfl, rfl, rfl, rfl, rfl⟩ with no lemmas, rewrites, or case splits. It is a pure status snapshot, not an analytic argument.
why it matters
Parent use is typedResidual_gap6_lookalike_decoys_fail, the R0 residual that packages lookalike-falsify certificates (3D Lorentzian continuation is not 4D action, 4D kinematical Wick is not action-level, hinge data and cm4 sign are not action-level) together with this post-close guard. Downstream doc: "R0 residual closed by the lookalike-falsify package."
In the Recognition gravity stack this is bookkeeping after the Gap-6 close, not a new dynamical law. It records that the V2 action-level Wick route discharged the campaign obligation while weaker lookalikes remain separated, and that the 3D Lorentzian-sector action bit is still open by design. Framework role is residual hygiene on the Seven Gaps ledger (post-F3 honesty patch), not a T0–T8 forcing step or a mass/alpha derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.