Pith. sign in
module module moderate

IndisputableMonolith.Verification.GWTC3RingdownStatus

show as:
view Lean formalization →

Catalogues GWTC-3 ringdown and GR-test status constants for the quantum-gravity falsifier register: analyzed event count, FAR threshold, graviton-mass bound, and flags for no post-merger echoes, no significant GR deviation, and QNM consistency with GR. Downstream likelihood aggregation imports this as the LIGO/Virgo observational layer. Structure is named data plus elementary positivity lemmas, not a deep derivation.

claimFixes GWTC-3 ringdown/GR-test parameters for the falsifier register: analyzed confident-signal count $N$, false-alarm-rate threshold, graviton mass bound $m_g$, and status flags (no post-merger echoes reported, no significant GR deviation reported, QNM spectrum consistent with GR), with elementary positivity facts $N>0$ and related bounds.

background

Recognition Science keeps a quantum-gravity falsifier register (master plan §7). The upstream module FalsifierRegisterDatasets attaches concrete named datasets and numerical sensitivity records to every register row, as a structural theorem layer with no sorry and no RS-internal axiom.

This module is the GWTC-3 attachment for ringdown and GR tests: the LIGO/Virgo/KAGRA O3 catalog subset used in published GR-consistency and echo searches. It records how many confident signals were analyzed, the FAR cut, a graviton-mass bound, and boolean status drawn from the catalog literature (no reported post-merger echoes, no significant GR deviation, QNM consistent with GR).

Sibling declarations are the constants themselves, positivity lemmas, and a bundled status-flag record. Values are definitional inputs to verification, not RS-derived predictions of waveforms.

proof idea

Definition and data-attachment module, not a theorem proof. It introduces named constants (event count, FAR threshold, graviton-mass bound, echo/QNM/GR status flags), proves elementary positivity or non-vacuity facts about those constants, and packages status flags for the register. No multi-step argument beyond norm_num-style or trivial inequality checks on the recorded numbers.

why it matters in Recognition Science

Supplies the GWTC-3 observational anchor so ringdown-related falsifier rows (echoes, QNM GR consistency, graviton mass) can be scored against published LIGO/Virgo constraints. Downstream, FalsifierLikelihoodRegister imports this module and aggregates Sessions 107--115 into the dataset-specific likelihood/status layer over the §7 register (also marked structural theorem, 0 sorry).

Without these constants the likelihood layer would lack a concrete GWTC-3 ringdown dataset handle. The module closes a verification bookkeeping gap rather than a forcing-chain step (T0--T8); it ties external GW catalog status into the RS falsifier pipeline.

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)