qnmAttachment
plain-language theorem explainer
Attaches the quasinormal-mode / ringdown falsifier-register row to LIGO/Virgo/KAGRA GWTC-3 tests of GR (with future LISA/ET as the high-precision channel). Sensitivity is the published graviton-mass bound 2.42×10⁻²³ eV/c²; the RS target scale is 0.2406, and current data are flagged not yet sensitive. Anyone auditing §7 QG falsifiability or the GWTC-3 ringdown certificate cites this record. It is a plain structure literal, not a proved claim.
Claim. The quasinormal-mode / ringdown discriminator row is the dataset attachment with sector label "Quasinormal-mode / ringdown discriminator", dataset "LIGO/Virgo/KAGRA GWTC-3 tests of GR; future LISA/Einstein Telescope", units "eV/c^2 graviton-mass bound", numerical sensitivity $2.42\times 10^{-23}$, RS target scale $0.2406$, and $\texttt{currentlySensitive}=\mathrm{false}$.
background
The module Quantum Gravity Falsifier Register Dataset Attachments wires named observational channels and numerical scales onto every row of the quantum-gravity master plan §7 falsifier register. Status is structural: zero sorry, zero new RS-internal axioms. A row is attached when it has a named dataset, a sensitivity scale, an RS target scale or band, and an honest flag for whether present data already reach that target. Purpose is falsifiability accounting, not empirical confirmation.
DatasetAttachment is the common record type: sector and dataset strings, a units string, real sensitivity and rsTargetScale (dimensionless unless units say otherwise), and a Boolean currentlySensitive. For several future-facing rows the flag is honestly false: the channel is named, but not yet precise enough for the φ-suppressed target.
Anchor context for this row comes from the module doc: GWTC-3 tests of GR report no significant deviations from GR, no post-merger echoes in analyzed events, and a graviton-mass bound $m_g \le 2.42\times 10^{-23},\mathrm{eV}/c^2$. Remnant consistency and lack of significant QNM deviation are the published qualitative status; LISA and Einstein Telescope are the named high-precision successors.
proof idea
Definition by structure literal. Each field of DatasetAttachment is filled with a concrete string or numeral: sector and dataset name the QNM/ringdown channel and GWTC-3 (plus future LISA/ET); units mark the graviton-mass bound; sensitivity is $2.42\times 10^{-23}$; rsTargetScale is $0.2406$; currentlySensitive is false. No tactics, no lemmas, no computation beyond the literal.
why it matters
This row is the QNM entry in the §7 falsifier-register dataset ledger. Downstream, qnm_sensitivity_pos and qnm_target_pos discharge positivity of sensitivity and RS target by unfolding this literal and norm_num. Those feed falsifier_dataset_register_one_statement and the master certificate FalsifierDatasetRegisterCert, which require every §7 row to carry a named dataset, positive sensitivity, and positive RS target scale.
Separately, GWTC3RingdownStatus reuses the attachment: gwtc3_qnm_dataset_positive packages the two positivity facts, and GWTC3RingdownStatusCert bundles them with event-count, FAR-threshold, and graviton-mass-bound positivity plus the echo-row attachment. In the broader RS picture this is verification infrastructure for ringdown / QNM discriminators against GR, not a derivation of the eight-tick octave or $D=3$; it only makes the observational test channel and the present precision gap explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.