gwtc3QNMConsistentWithGR
plain-language theorem explainer
Boolean status flag recording that LIGO/Virgo/KAGRA GWTC-3 reports remnant quasi-normal-mode consistency with general relativity. Verification and falsifier-register authors cite it when assembling the GWTC-3 ringdown status certificate. It is a one-line constant definition equal to true, not a derived physical theorem.
Claim. The published GWTC-3 qualitative status that remnant quasi-normal modes are consistent with general relativity is recorded as the Boolean value $\mathrm{true}$.
background
The module attaches a concrete GWTC-3 status record to the §7 echo/QNM falsifier rows. It is not posterior ingestion: it freezes published scalar and qualitative facts from the LIGO/Virgo/KAGRA GWTC-3 tests of GR (O3b subset) so they can be referenced inside the Lean verification layer.
Among those published facts are: 15 confident signals with false-alarm rates at most $10^{-3},\mathrm{yr}^{-1}$; no significant evidence for physics beyond GR; no post-merger echoes in the analyzed events; remnant/QNM consistency with GR; and a graviton mass bound $m_g \le 2.42\times 10^{-23},\mathrm{eV}/c^2$.
RS structural targets for later likelihood-style tests (echo damping ratio $1/\varphi$, rung phase delay $\log\varphi$, leading-log coefficient $c_{\mathrm{RS}}$) sit outside this flag. This definition only stores the published QNM-consistency status bit.
proof idea
There is no proof. The declaration is a Boolean definition whose body is the literal true, encoding the published qualitative status as a constant. Downstream theorems such as gwtc3_status_flags discharge equalities to true by reflexivity (rfl).
why it matters
The flag is one of three qualitative status bits bundled by gwtc3_status_flags (no post-merger echoes, no significant GR deviation, QNM consistent with GR), all recorded true. That conjunction feeds the master structure GWTC3RingdownStatusCert and the one-statement attachment theorem gwtc3_ringdown_status_one_statement.
In the Recognition Science verification stack this closes a structural bookkeeping step: the §7 echo/QNM falsifier register can see that the public GWTC-3 abstract reports remnant/QNM consistency with GR. It does not yet test RS-specific ringdown predictions against GWTC-3 posterior files; that remains an open data-analysis path outside this constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.