gwtc3_echo_dataset_positive
plain-language theorem explainer
The GWTC-3 echo phenomenology row carries strictly positive instrumental sensitivity and a strictly positive RS target scale. Ringdown-status and §7 falsifier assembly cite it to certify that the echo attachment is numerically well-posed. The proof is a one-line pairing of the two positivity lemmas already proved on that attachment.
Claim. The echo phenomenology dataset attachment satisfies both positivity predicates: its reported sensitivity is positive and its RS target scale is positive (the dimensionless echo amplitude ratio $1/\varphi \approx 0.618$).
background
This module records published GWTC-3 ringdown/echo/QNM status facts against the §7 falsifier register. It is a structural status certificate, not posterior ingestion: the public abstract reports no post-merger echoes in the analyzed O3b events, remnant/QNM consistency with GR, and related scalar bounds.
The echo attachment is the register row for black-hole echo phenomenology on the LIGO/Virgo/KAGRA GWTC-3 tests-of-GR dataset. Units are echo amplitude ratio; the recorded sensitivity is $0.10$ and the RS target scale is $0.618$, matching the RS echo damping ratio $1/\varphi$. Two upstream lemmas already assert that this sensitivity and this target scale are positive.
HasPositiveSensitivity and HasPositiveTargetScale are the register predicates that a dataset row must meet before it can enter a status certificate.
proof idea
Term-mode pairing. The proof is the anonymous constructor ⟨echo_sensitivity_pos, echo_target_pos⟩, which discharges the two conjuncts by the pre-proved positivity lemmas on echoAttachment. No further algebra or case analysis.
why it matters
Feeds the field echo_dataset_positive of gwtc3RingdownStatusCert, the module-level status record that packages GWTC-3 event-count, FAR threshold, graviton-mass bound, echo, and QNM positivity into one certificate.
In the Recognition framework this closes the structural half of the §7 echo falsifier row: the RS target is the dimensionless damping ratio $1/\varphi \approx 0.618$ (with companion rung phase delay $\log\varphi$ and leading-log coefficient $c_{RS}$). The certificate records that GWTC-3 reports no post-merger echoes while keeping the RS scale numerically live for later likelihood-style tests against the public posterior release. Zero sorry; zero new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.