Pith. sign in
module module high

IndisputableMonolith.Verification.GWTC3RingdownStatus

show as:
view Lean formalization →

GWTC-3 ringdown status bundle for the quantum-gravity falsifier register: event counts, FAR threshold, graviton-mass bound, and boolean flags that no post-merger echoes or significant GR deviations were reported and that QNMs match GR. Verification authors cite it when wiring LIGO/Virgo catalog facts into dataset attachments. Content is definitional constants plus elementary positivity and flag lemmas.

claimRecord the GWTC-3 GR-tests ringdown dataset: analyzed confident-signal count $N>0$, false-alarm-rate threshold $\mathrm{FAR}_*>0$, graviton-mass bound $m_g^{\mathrm{bound}}>0$, and status flags (no post-merger echoes reported; no significant GR deviation reported; QNM spectrum consistent with GR), with positivity of the echo and QNM dataset attachments.

background

Recognition Science maintains a quantum-gravity master-plan §7 falsifier register: named observational channels that could defeat RS or GR-extension claims. The upstream module FalsifierRegisterDatasets attaches concrete named datasets and numerical sensitivity records to every register row (structural theorem, zero sorry).

This module specializes that attachment layer to the LIGO/Virgo/KAGRA GWTC-3 catalog ringdown and GR-tests subset. It freezes catalog-facing scalars (analyzed event count, FAR threshold, published graviton-mass bound) and boolean status summaries: whether post-merger echoes were reported, whether significant GR deviations were claimed, and whether quasinormal-mode (QNM) fits remain consistent with GR Kerr ringdown.

Sibling lemmas assert positivity of the numeric thresholds and of the echo/QNM dataset attachments, and package the booleans into a compact status-flag record consumed by the likelihood layer.

proof idea

Definition module with thin certificate lemmas, not a deep derivation. Numeric parameters are closed definitions; positivity facts are immediate from the chosen positive literals. Status flags are boolean constants reflecting the published GWTC-3 GR-tests summary (no echoes, no significant GR deviation, QNM-consistent). Dataset-positivity lemmas discharge the non-emptiness side conditions expected by the falsifier register attachments. No analytic GR or waveform proof lives here.

why it matters in Recognition Science

Feeds the downstream FalsifierLikelihoodRegister, which aggregates Sessions 107--115 into the dataset-specific likelihood and status layer over master-plan §7 (also a structural theorem, zero sorry). Without a frozen GWTC-3 ringdown status bundle, echo and QNM falsifier rows lack a citable observational anchor.

In the broader RS verification story this is empirical bookkeeping, not a forcing-chain step (T0--T8). It lets the register state, in Lean, that current GWTC-3 public summaries do not report the echo or GR-break signatures that would pressure RS or modified-gravity ringdown claims, while recording the graviton-mass bound and event-count sensitivity of that statement.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (16)