gwtc3_ringdown_status_one_statement
plain-language theorem explainer
Packages the published GWTC-3 ringdown/echo/QNM status facts into a single conjunction: positive event count, FAR threshold, and graviton-mass bound; three true qualitative flags (no echoes, no significant GR deviation, QNM consistent with GR); and a nonempty status certificate. Verification authors cite it when attaching the LIGO/Virgo/KAGRA GWTC-3 GR-tests abstract to the §7 falsifier register. The proof is a term that packs three positivity lemmas, three definitional equalities, and the certificate inhabitant.
Claim. The GWTC-3 analyzed-event count is positive, the false-alarm-rate threshold is positive, the published graviton-mass bound is positive, the flags "no post-merger echoes reported", "no significant GR deviation reported", and "QNM consistent with GR" all hold, and the GWTC-3 ringdown status certificate type is inhabited.
background
This module records a structural status attachment for the LIGO/Virgo/KAGRA GWTC-3 tests of general relativity. It is not posterior ingestion: it freezes the public abstract scalars and qualitative claims so they can sit on the §7 echo/QNM falsifier rows.
Concrete constants in the module: analyzed confident signals $N = 15$; FAR threshold $10^{-3},\mathrm{yr}^{-1}$; graviton mass bound $m_g \le 2.42\times 10^{-23},\mathrm{eV}/c^2$. Three Boolean status defs are definitionally true: no post-merger echoes reported, no significant GR deviation reported, and remnant/QNM consistency with GR.
The master structure GWTC3RingdownStatusCert bundles positivity of those three scalars, positive-sensitivity/target-scale witnesses for the echo and QNM dataset attachments, and the three status flags. Upstream positivity lemmas discharge $0 < N$, $0 < \mathrm{FAR}$, and $0 < m_g$ by decide/norm_num after unfolding the numeric defs.
proof idea
Term-mode packing of an already-proved conjunction. The seven conjuncts are filled by: gwtc3AnalyzedEventCount_pos, gwtc3FalseAlarmRateThreshold_pos, gwtc3GravitonMassBound_pos (each a short unfold-and-decide/norm_num proof of positivity); three rfl steps for the Boolean status flags (they are definitionally true); and gwtc3RingdownStatusCert_inhabited, which supplies a witness of Nonempty GWTC3RingdownStatusCert. No further rewriting or case analysis.
why it matters
Closes the GWTC-3 ringdown/echo/QNM status attachment as a structural theorem (module status: 0 sorry, 0 new RS-internal axioms, closure dated 2026-05-22). It upgrades the §7 falsifier-register rows with a single citeable one-statement fact rather than a scatter of defs.
RS structural targets named in the module (echo damping $1/\varphi \approx 0.618$, rung phase delay $\log\varphi \approx 0.481$, leading-log $c_{RS}\approx -0.2406$) are the intended comparison scales once full posterior files are analyzed; this theorem does not perform that comparison. It only certifies that the published GWTC-3 abstract facts are recorded and that the certificate type is inhabited.
No downstream dependents are wired yet (used_by empty). The natural parent is any register-level theorem that needs a single GWTC-3 status hypothesis rather than six separate facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.