qnm_sensitivity_pos
plain-language theorem explainer
The quasinormal-mode / ringdown falsifier row carries a strictly positive numerical sensitivity (the GWTC-3 graviton-mass bound scale). Anyone assembling the quantum-gravity falsifier register certificate or the GWTC-3 ringdown status bundle cites this. The proof is a two-step unfold-and-norm_num check that the stored sensitivity is positive.
Claim. The quasinormal-mode dataset attachment $D_{\mathrm{QNM}}$ satisfies $0 < D_{\mathrm{QNM}}.\mathrm{sensitivity}$, i.e. its recorded numerical sensitivity scale is strictly positive.
background
The module attaches named observational channels and numerical sensitivity records to every row of the quantum-gravity master-plan §7 falsifier register. Attachment is structural accounting: a named dataset, a sensitivity scale, an RS target scale or band, and an honest flag on whether current data already reach the RS target. Records do not claim empirical confirmation of RS.
HasPositiveSensitivity is the predicate $0 < D.\mathrm{sensitivity}$ on a DatasetAttachment. The QNM row stores sector "Quasinormal-mode / ringdown discriminator", dataset "LIGO/Virgo/KAGRA GWTC-3 tests of GR; future LISA/Einstein Telescope", units "eV/c^2 graviton-mass bound", sensitivity $2.42\times 10^{-23}$, and RS target scale $0.2406$. The sensitivity number is the published GWTC-3 graviton-mass bound used as the concrete current scale.
proof idea
Unfold the positive-sensitivity predicate and the QNM attachment record, exposing the concrete inequality $0 < 2.42\times 10^{-23}$. Discharge it by norm_num. No lemmas beyond definitional unfolding are required.
why it matters
This is one of the per-row positivity lemmas that populate the falsifier dataset register certificate and the one-statement conjunction asserting every register row has positive sensitivity and positive RS target scale. Downstream, gwtc3_qnm_dataset_positive packages it with the matching target-scale positivity fact for the GWTC-3 ringdown status module.
In the broader RS verification story the QNM/ringdown discriminator is the post-merger channel that future LISA/ET precision is meant to stress; the present lemma only locks the accounting invariant that the stored sensitivity is a positive real, so the register cannot silently carry a zero or negative scale. It does not itself encode the eight-tick octave or the forcing chain; it is pure falsifiability bookkeeping for the QG plan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.