gwtc3RingdownStatusCert
plain-language theorem explainer
A packaged certificate that the GWTC-3 ringdown/echo/QNM status record is fully inhabited: analyzed event count, FAR threshold, and graviton mass bound are positive; echo and QNM attachments have positive sensitivity and target scale; and the three published qualitative flags hold. Verification authors cite it when wiring LIGO/Virgo/KAGRA O3b status into the §7 falsifier rows. Construction is a structure instance that wires six already-proved positivity and flag lemmas.
Claim. There is a GWTC-3 ringdown status certificate whose fields assert: analyzed event count $>0$; false-alarm-rate threshold $>0$; graviton mass bound $>0$; the echo attachment has positive sensitivity and positive target scale; the QNM attachment has positive sensitivity and positive target scale; and the published flags record no post-merger echoes, no significant GR deviation, and QNM consistency with GR.
background
This module attaches published GWTC-3 (LIGO/Virgo/KAGRA O3b) ringdown status facts to the Recognition Science §7 echo/QNM falsifier register. It is a structural status cert, not posterior ingestion. The public abstract reports 15 confident signals with FAR $\le 10^{-3},\mathrm{yr}^{-1}$, no significant evidence beyond GR, no post-merger echoes, remnant/QNM consistency with GR, and graviton mass bound $m_g \le 2.42\times 10^{-23},\mathrm{eV}/c^2$.
The master structure packages six obligations: positivity of the analyzed event count, FAR threshold, and graviton mass bound; positive sensitivity and target scale on the echo and QNM dataset attachments; and three qualitative status flags set true. RS structural targets reserved for later full testing include echo damping ratio $1/\varphi \approx 0.618$, rung phase delay $\log\varphi \approx 0.481$, and leading-log coefficient $c_{RS}\approx -0.2406$.
Upstream lemmas discharge each field by decide/norm_num on the numeric constants, or by pairing the attachment positivity theorems for the echo and QNM rows.
proof idea
Structure-instance assembly, not a tactic proof. Each field is filled by a named sibling lemma: event-count positivity (unfold + decide), FAR-threshold positivity (unfold + norm_num), graviton-mass-bound positivity (unfold + norm_num), echo-row positive sensitivity and target scale (pair of attachment lemmas), QNM-row positive sensitivity and target scale (pair of attachment lemmas), and the three qualitative status flags (triple of rfl equalities). No new arithmetic or case analysis appears here.
why it matters
Master cert of the GWTC-3 ringdown status module. Downstream, the inhabitedness theorem uses this value to prove Nonempty of the certificate type, giving a one-statement attachment result for the verification layer. It upgrades the §7 echo/QNM falsifier rows with concrete published GWTC-3 scalars and flags, closing the structural (non-posterior) half of the ringdown status attachment. Full likelihood-style tests of RS echo predictions (damping $1/\varphi$, phase $\log\varphi$) remain outside this cert and require the GWTC-3 posterior release files. Zero sorry and zero new RS-specific axioms in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.