gwtc3FalseAlarmRateThreshold
plain-language theorem explainer
Records the GWTC-3 O3b false-alarm-rate cut as the real constant 10^{-3} per year. Anyone citing the ringdown/echo status attachment or the master GWTC-3 cert uses this scalar. The body is a bare numeric definition, not a derived claim.
Claim. The false-alarm-rate threshold for the analyzed GWTC-3 O3b subset is the real number $10^{-3}\,\mathrm{yr}^{-1}$.
background
The module attaches published LIGO/Virgo/KAGRA GWTC-3 tests-of-GR status facts to the §7 echo/QNM falsifier register. It is a status certificate, not posterior ingestion: the public abstract reports 15 confident signals in the O3b subset with false alarm rates at most $10^{-3},\mathrm{yr}^{-1}$, no significant beyond-GR evidence, no post-merger echoes, QNM consistency with GR, and a graviton mass bound.
This definition freezes that FAR cut as a named real constant in $\mathrm{yr}^{-1}$. Sibling scalars cover analyzed event count, graviton mass bound, and boolean status flags (no echoes, no GR deviation, QNM consistent with GR). RS structural targets elsewhere in the module (echo damping $1/\varphi$, rung phase $\log\varphi$, leading-log $c_{RS}$) are not encoded in this constant.
proof idea
No proof. The declaration is a one-line real definition equal to 1e-3. Downstream positivity is discharged by unfolding and norm_num.
why it matters
Feeds three local consumers: the positivity lemma for the FAR threshold, the master structure GWTC3RingdownStatusCert (field far_threshold_pos), and the bundled one-statement status theorem that conjoins event-count, FAR, graviton-mass, and qualitative GR/echo/QNM flags.
In the Recognition verification layer this pins the published selection cut used when the §7 echo/QNM falsifier rows are upgraded with a concrete GWTC-3 record. It does not test RS echo predictions (damping $1/\varphi$, phase $\log\varphi$); those need the posterior release files. Closure note in the module: structural theorem, zero sorry, zero new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.