gwtc3AnalyzedEventCount_pos
plain-language theorem explainer
The GWTC-3 GR-tests subset has a strictly positive count of confident signals (the published figure is 15). Anyone assembling the ringdown/echo/QNM status certificate or the one-statement GWTC-3 attachment cites this positivity lemma. The proof unfolds the constant definition and discharges 0 < 15 by kernel decision.
Claim. The number of confident signals analyzed in the relevant GWTC-3 tests-of-GR subset is strictly positive: $0 < N_{\mathrm{GWTC3}}$, where $N_{\mathrm{GWTC3}} = 15$.
background
This module attaches a concrete LIGO/Virgo/KAGRA GWTC-3 status record to the §7 echo/QNM falsifier rows. It is a structural status certificate, not posterior ingestion: it records published scalar and boolean facts from the public GWTC-3 GR-tests abstract and wires them into the verification register.
The analyzed-event count is the natural-number constant equal to 15, matching the public report of 15 confident signals in the O3b subset with false-alarm rates at most $10^{-3},\mathrm{yr}^{-1}$. Sibling constants cover the FAR threshold, the graviton-mass bound, and boolean flags for no reported post-merger echoes, no significant GR deviation, and QNM consistency with GR.
RS structural targets mentioned in the module (echo damping $1/\varphi$, rung phase delay $\log\varphi$, leading-log coefficient $c_{\mathrm{RS}}$) are context only; this lemma is purely the positivity of the event count.
proof idea
Term-mode proof by unfolding the definition of the analyzed-event count (the constant 15) and applying decide, which closes the decidable inequality $0 < 15$ in the kernel. No external lemmas are required.
why it matters
Positivity of the event count is a field of the GWTC-3 ringdown status certificate structure: that certificate packs event-count positivity together with FAR-threshold positivity, graviton-mass-bound positivity, and the echo/QNM dataset-positive flags. The same inequality appears as the first conjunct of the one-statement GWTC-3 status attachment theorem, which conjoins all published scalar and boolean status facts into a single Prop.
In the Recognition verification layer this closes a structural precondition for treating the GWTC-3 GR-tests subset as a nonempty observational handle on the §7 echo/QNM falsifier rows. It does not itself test RS echo predictions (damping $1/\varphi$, phase delay $\log\varphi$); those remain open pending posterior-file analysis. Zero sorry, zero new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.