gwtc3NoPostMergerEchoesReported
plain-language theorem explainer
Boolean status flag recording that LIGO/Virgo/KAGRA GWTC-3 published no post-merger echoes in the analyzed O3b events. Downstream ringdown certificates and the one-statement status theorem cite it as a qualitative GR-consistency input. The body is the constant true, not a derived proof.
Claim. The published GWTC-3 qualitative status that no post-merger echoes were reported in the analyzed events is recorded as $\mathsf{true}$.
background
The module attaches a concrete GWTC-3 status record to the §7 echo/QNM falsifier rows. It is not posterior ingestion: it stores published scalar and qualitative facts from the LIGO/Virgo/KAGRA GWTC-3 tests of GR (15 confident O3b signals with FAR $\le 10^{-3},\mathrm{yr}^{-1}$, no significant beyond-GR evidence, remnant/QNM consistency with GR, and a graviton-mass bound).
In Recognition Science, post-merger echoes are a structural target with damping ratio $1/\varphi\approx 0.618$, rung phase delay $\log\varphi\approx 0.481$, and leading-log coefficient $c_{\mathrm{RS}}\approx -0.2406$. This flag only records the published null report; full likelihood tests against those RS scales need the GWTC-3 posterior release files.
Sibling flags cover QNM consistency with GR and absence of significant GR deviations. Upstream status strings elsewhere in the monolith (native units, discrete Lichnerowicz sector claims) are unrelated bookkeeping; this definition is local dataset metadata.
proof idea
Definitional constant: the value is literally true. No tactics, no lemmas, no reduction. Downstream theorems such as gwtc3_status_flags discharge equalities to true by rfl.
why it matters
Closes one qualitative cell of the GWTC-3 ringdown status attachment used by the master certificate GWTC3RingdownStatusCert and by gwtc3_ringdown_status_one_statement, which conjoins event-count positivity, FAR threshold positivity, graviton-mass bound positivity, and the three qualitative true flags (no echoes, no significant GR deviation, QNM consistent with GR).
In the RS verification layer this ties the §7 echo falsifier row to a named public catalog rather than an abstract placeholder. It does not yet test the RS echo scales ($1/\varphi$ damping, $\log\varphi$ delay) against strain posteriors; the module doc marks that as future work on the IGWN GWTC-3 TGR release. Relative to the forcing chain, it is observational bookkeeping, not a T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.