pta_target_pos
plain-language theorem explainer
The PTA stochastic-background attachment carries a strictly positive RS target scale (0.481, from log φ). Anyone wiring NANOGrav/EPTA rows into the falsifier register or likelihood status theorems cites this. The proof is a two-step unfold-and-norm_num check that the recorded target is positive.
Claim. The pulsar-timing-array dataset attachment (NANOGrav 15-year + EPTA DR2 nanohertz stochastic background) has positive RS target scale: its recorded target $0.481$ satisfies $0 < 0.481$.
background
This module attaches named observational channels, numerical sensitivities, and RS target scales to every row of the quantum-gravity master-plan §7 falsifier register. Attachment is structural accounting only: a named dataset, a sensitivity, an RS target or band, and an honest currently-sensitive flag. No row claims empirical confirmation of RS.
HasPositiveTargetScale is the predicate $0 < D.\mathrm{rsTargetScale}$ on a DatasetAttachment record. The PTA row (ptaAttachment) records the NANOGrav 15-year / EPTA DR2 nanohertz stochastic background, with units on the spectral-index scale, sensitivity $0.80$, and RS target scale $0.481$. That target is the structural $\log\varphi$ signature noted in the attachment doc; the row is attached but not yet dynamically matched to the full spectrum, and is marked not currently sensitive.
proof idea
Term-mode proof by unfolding. Expand HasPositiveTargetScale to the inequality $0 < D.\mathrm{rsTargetScale}$, then unfold ptaAttachment so the target field is the concrete numeral $0.481$. norm_num discharges $0 < 0.481$. No lemmas beyond definitional unfolding.
why it matters
Feeds the PTA status theorems in the EPTA and NANOGrav likelihood modules: both epta_dataset_attachment_status and nanograv_dataset_attachment_status package positive sensitivity, positive target scale, and currentlySensitive = false as a single conjunction, using this lemma as the middle conjunct. It is also one of the target-positivity fields collected by falsifierDatasetRegisterCert, the module-level certificate that every register row has a positive sensitivity and positive RS target.
In the broader RS picture this is falsifiability bookkeeping for the PTA stochastic-background channel, not a dynamical derivation of the Hellings–Downs spectrum. The target $0.481 \approx \log\varphi$ is the φ-rational structural marker; closing a full spectral match remains open. The module itself is a structural theorem (zero sorry, zero RS-internal axioms).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.