qnm_target_pos
plain-language theorem explainer
The quasinormal-mode ringdown dataset attachment carries a strictly positive RS target scale. Citers of the falsifier-register certificate and the GWTC-3 ringdown positivity lemma need this fact. The proof unfolds the attachment record and closes the inequality by numerical normalization.
Claim. The quasinormal-mode / ringdown discriminator attachment has positive RS target scale, i.e. $0 < 0.2406$ (in the attachment's target units).
background
This module attaches named observational channels, sensitivity scales, and RS target scales to every row of the quantum-gravity master-plan §7 falsifier register. Attachments are structural accounting records: they name which experiment tests which prediction and at what reported precision. They do not claim empirical confirmation of RS.
HasPositiveTargetScale is the predicate $0 < D.\mathrm{rsTargetScale}$ on a DatasetAttachment. The QNM attachment records the GWTC-3 tests-of-GR channel (LIGO/Virgo/KAGRA; future LISA/ET), stores the published graviton-mass bound $2.42\times 10^{-23},\mathrm{eV}/c^2$ as the sensitivity scale, and sets the RS target scale to $0.2406$.
proof idea
One-line tactic proof: unfold the positivity predicate and the QNM attachment record, then norm_num discharges $0 < 0.2406$. No lemmas beyond definitional unfolding.
why it matters
Feeds the aggregate falsifier-register certificate (falsifierDatasetRegisterCert), which bundles positivity of sensitivity and target for every attached row. Also feeds gwtc3_qnm_dataset_positive, which packages QNM sensitivity and target positivity as a single GWTC-3 ringdown status fact. Within the register this is the ringdown/QNM discriminator row: GWTC-3 reports remnant consistency and no significant QNM deviation, with future LISA/ET as the high-precision channel. The positivity lemmas keep the certificate free of sorry and free of new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.