Gap6LedgerTerminalGuard
plain-language theorem explainer
A five-conjunct ledger guard recording the post-F3 Gap6 close: the full-theory Lorentzian-action benchmark is true, campaign and 4D simplex action-open flags are cleared, kinematical Wick is certified, and the 3D Lorentzian-sector action bit stays open. Downstream residual and terminal theorems cite it as the post-close witness. It is a pure Prop abbreviation of status-field equalities.
Claim. The Gap-6 ledger terminal guard holds when all of the following are true: the full-theory benchmark for Lorentzian action recovery is set; the campaign flag that Gap-6 action continuation is open is false; the 4D causal-simplex flag that action-level continuation is open is false; the Lorentzian-sector flag that Lorentzian action continuation is open remains true; and the campaign flag that Gap-6 kinematical Wick is certified is true.
background
Wave C4 R0 packages lookalike-falsify receipts for Gap 6 in the seven-gaps gravity campaign. After F3 (2026-07-23), Gap 6 closed via the V2 Wick action continuation; this module keeps separation certificates so banked lookalikes are not mistaken for that closer.
Status records are pure data defs: fullTheoryBenchmarks tracks which continuum/action recoveries have flipped; sevenGapsCampaignStatus is the campaign outcome board; causalSimplex4DStatus and lorentzianSectorStatus report 4D simplex and Lorentzian-sector deliverables. Upstream snippets still show some action-open bits true in their home modules; the guard asserts the post-close values expected after the V2 flip (Gap-6 action true, campaign and 4D action-open cleared, kinematical Wick certified, 3D sector action still open).
The guard is the Prop shape of that post-close ledger snapshot, not a dynamical theorem.
proof idea
Definition only: the body is the five-way conjunction of boolean field equalities on the four status records. No tactics, no lemmas. The inhabiting theorem gap6LedgerTerminalGuard later discharges it by five rfl steps against the concrete status values in scope.
why it matters
After F3 closed Gap 6 through wick_action_continuation_4d_v2, the campaign needed a machine-checkable post-close snapshot so lookalike certificates stay honest. This guard is that snapshot. It feeds gap6LedgerTerminalGuard (the trivial witness theorem) and sits inside TypedResidual_gap6_lookalike_decoys_fail, the DAG R0 residual that packages all lookalike separations plus the post-F3 V2 ledger close.
In the Recognition gravity stack this is bookkeeping for the Lorentzian action-continuation gap on the causal simplex / Wick side, not a new continuum limit. It records that action-level 4D continuation is no longer open at campaign and 4D-simplex level while the 3D Lorentzian-sector action bit remains deliberately open, matching the doc-comment honesty patch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.