IndisputableMonolith.Gravity.SevenGaps.WickActionV2CloseStatus
Status ledger for Gap 6 of the QG seven-gaps campaign: whether the Lorentzian Wick-action V2 certificate family is closed. It packages boolean flags (both halves green, action bound linked to V2) as a machine-checked close-status record, proved by reflexivity on assembled certificates. Gravity auditors and the full-theory ledger cite it; the audit module imports it for axiom hygiene.
claimA machine-checked close-status record for Gap 6 (Wick-action continuation, V2): boolean flags recording that the Lorentzian action bound is tied to the V2 certificate family and that both halves of the gap are green, under the assembled causal Wick-action certificates (with coupling threshold $7/12 < \alpha$).
background
The QG seven-gaps campaign tracks scoped increments toward quantum-gravity closure without flipping full-strength QGScopeAudit flags. Gap 6 is the Lorentzian-sector Wick-action lane: lift causal (CDT-style) simplex structure to a continuation certificate for the action.
Upstream, CausalSimplex4D supplies the 4D causal 4-simplex classes and kinematical Wick rotation. WickActionCertFamilyAssembly binds those ingredients into the V2 succession certificate family under $7/12 < \alpha$. CampaignLedger and FullTheoryLedger are the campaign-wide and full-theory boolean ledgers; this module is the Gap-6 V2 slice of that pattern.
The module itself is flag-block documentation: named status objects whose truth is definitional equality to the assembled certificates, discharged by rfl.
proof idea
Definition-and-status module, not a deep proof development. Close-status records and flag tuples are defined from the imported V2 certificate assembly and ledger conventions. Equalities such as flag unpacking and "both halves green" are one-line rfl against those definitions. Linking lemmas only restate that the Lorentzian action-bound obligation is the V2 family already assembled upstream; no new analytic estimate is proved here.
why it matters in Recognition Science
Gap 6 is the Wick-action half of the Lorentzian QG lane. This module is the campaign's machine-readable answer to "is V2 closed at the scoped increment?" so CampaignLedger / full-theory bookkeeping can cite a single status object rather than raw certificate terms.
It is imported by WickActionV2CloseStatusAudit, whose job is axiom hygiene: headline theorems must stay inside [propext, Classical.choice, Quot.sound] with zero sorryAx. In the Recognition gravity stack it sits downstream of the 4D causal-simplex Wick lift and the V2 cert family assembly, and upstream of audit and ledger rollups. It does not claim full physical closure of quantum gravity; only the scoped V2 flag block.
scope and limits
- Does not prove a new Lorentzian action bound; only records status of the assembled V2 family.
- Does not flip full-strength QGScopeAudit closure flags.
- Does not establish full physical QG closure; scoped campaign increment only.
- Does not re-derive 4D causal simplex or Wick rotation; imports those modules.
- Does not weaken the $7/12 < \alpha$ threshold fixed by the V2 assembly.