gwtc3FalseAlarmRateThreshold_pos
plain-language theorem explainer
The GWTC-3 false-alarm-rate threshold used for the O3b subset is strictly positive. Anyone assembling the ringdown/echo status certificate or the one-statement GWTC-3 attachment cites this fact. The proof unfolds the numeric definition $10^{-3}\,\mathrm{yr}^{-1}$ and discharges positivity by arithmetic normalization.
Claim. The published GWTC-3 false-alarm-rate threshold for the analyzed O3b subset satisfies $0 < 10^{-3}$ (in $\mathrm{yr}^{-1}$).
background
The module attaches a concrete GWTC-3 status record to the §7 echo/QNM falsifier rows. It records published LIGO/Virgo/KAGRA scalars from the GWTC-3 tests of GR: fifteen 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.
The false-alarm-rate threshold is the real constant $1\times 10^{-3}$ (units $\mathrm{yr}^{-1}$) taken from that public abstract. The module is a status certificate, not posterior ingestion; full likelihood tests of RS echo/QNM targets (damping $1/\varphi$, rung delay $\log\varphi$, leading-log $c_{RS}$) still need the GWTC-3 posterior release files.
proof idea
One-line arithmetic certificate. Unfold the definition of the threshold to the literal real $1\mathrm{e}{-3}$, then apply norm_num to obtain $0 < 10^{-3}$. No external lemmas beyond the definition itself.
why it matters
Positivity of the FAR threshold is a field of the GWTC-3 ringdown status certificate structure, wired in as far_threshold_pos. The same inequality appears as a conjunct in the one-statement GWTC-3 status attachment theorem, which packages event-count positivity, FAR positivity, graviton-mass-bound positivity, and the published no-echo / no-GR-deviation / QNM-consistent flags.
In the Recognition verification layer this closes a structural precondition for treating the GWTC-3 abstract as a well-formed positive dataset handle against the §7 echo and QNM falsifier rows. It does not itself test the RS targets (echo damping $1/\varphi\approx 0.618$, rung phase delay $\log\varphi\approx 0.481$); those remain open pending posterior-level analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.