gwtc3NoSignificantGRDeviationReported
plain-language theorem explainer
Boolean status flag recording the published GWTC-3 finding that there is no significant support for physics beyond general relativity. Verification and falsifier-register authors cite it when assembling the ringdown/echo/QNM status certificate. It is a one-line definition fixed to true, not a derived theorem.
Claim. The published GWTC-3 qualitative status "no significant support for physics beyond GR" is recorded as the Boolean value $\mathrm{true}$.
background
The module attaches a concrete GWTC-3 status record to the §7 echo/QNM falsifier rows. It is a structural status certificate, not posterior ingestion: it freezes the public LIGO/Virgo/KAGRA GWTC-3 abstract facts (15 confident O3b signals with FAR $\le 10^{-3},\mathrm{yr}^{-1}$, no significant beyond-GR evidence, no post-merger echoes, remnant/QNM consistency with GR, graviton mass bound $m_g \le 2.42\times 10^{-23},\mathrm{eV}/c^2$).
RS structural targets named in the module (echo damping $1/\varphi$, rung phase delay $\log\varphi$, leading-log $c_{RS}$) are context only; this flag does not encode those numbers. Upstream status strings from RS-native units, four-tet signed deficit, discrete Lichnerowicz, and alignment modules are dependency edges for the broader verification graph, not inputs to the Boolean itself.
proof idea
Definitional constant: the body is the literal Boolean true. No tactics, no lemmas, no reduction. Downstream theorems such as gwtc3_status_flags discharge equalities to true by rfl.
why it matters
Feeds the master structure GWTC3RingdownStatusCert and the bundled theorems gwtc3_status_flags and gwtc3_ringdown_status_one_statement, which package event-count positivity, FAR threshold, graviton-mass bound, and the three qualitative flags (no echoes, no significant GR deviation, QNM consistent with GR). It closes the published-status half of the §7 register attachment for beyond-GR deviation. Full likelihood tests of RS echo/QNM predictions (damping $1/\varphi$, phase $\log\varphi$) remain outside this cert and need the GWTC-3 posterior release files. Landmark link is verification hygiene, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.