pta_sensitivity_pos

The module attaches named observational channels and numerical sensitivity records to every row of the quantum-gravity master-plan §7 falsifier register. Attachment means a named dataset, a sensitivity scale, an RS target scale or band, and an honest flag for whether current data already reach the RS target. The purpose is falsifiability accounting, not empirical confirmation.

A dataset attachment is a record with sector, dataset name, units, sensitivity, and RS target scale. Positive sensitivity is the proposition that the recorded sensitivity is strictly greater than zero. The PTA row records the NANOGrav 15-year Hellings–Downs correlated background (68 pulsars, 15 yr baseline) together with EPTA DR2, with sensitivity $0.80$ and RS structural target $\log\varphi\approx 0.481$ as a $\varphi$-rational signature; the row is attached but not yet dynamically matched to the full spectrum.

Unfold the positive-sensitivity predicate and the PTA attachment record, then discharge $0 < 0.80$ by norm_num. No lemmas beyond definitional unfolding are required.

This lemma is one of the atomic positivity facts that close the falsifier-register certificate. It is packed into the one-statement theorem that every register row has positive sensitivity and positive RS target scale, and into the certificate structure that bundles all such positivity proofs.

Downstream, both the EPTA and NANOGrav likelihood modules quote it in their dataset-attachment status theorems, which assert that the PTA attachment is present, has positive sensitivity and positive target scale, and is explicitly marked not currently sensitive. That status is the honest accounting line for the nanohertz stochastic background against the RS $\log\varphi$ structural target, keeping the register conservative rather than confirmatory.