ptaAttachment
plain-language theorem explainer
Registers the PTA nanohertz stochastic-background channel (NANOGrav 15-year plus EPTA DR2) as a falsifier-register row with sensitivity 0.80, RS target scale log φ ≈ 0.481, and an honest not-yet-sensitive flag. Cosmology and PTA likelihood authors cite it when wiring spectral-index comparisons. The body is a pure structure literal, no proof obligations.
Claim. The PTA stochastic gravitational-wave background row is the dataset attachment with sector ``PTA stochastic gravitational-wave background'', dataset ``NANOGrav 15-year + EPTA DR2 nanohertz stochastic background'', units ``spectral-index scale'', sensitivity $0.80$, RS target scale $0.481$ (the structural $\log\varphi$ signature), and $\mathrm{currentlySensitive}=\mathrm{false}$.
background
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 that target. Purpose is falsifiability accounting, not empirical confirmation.
A dataset attachment is a six-field record: sector string, dataset string, units string, dimensionless (unless units say otherwise) sensitivity and RS target scale, and a Boolean currently-sensitive flag. For several future rows the flag is honestly false: the channel is named but not yet precise enough to test a φ-suppressed target.
This PTA row records the Hellings–Downs correlated nanohertz background from NANOGrav 15-year (68 pulsars, 15 yr) and EPTA DR2, with power-law spectrum compatible with the SMBHB reference slope $\gamma=13/3$. The RS structural target is $\log\varphi\approx 0.481$, a positive φ-rational signature on the spectral-index scale; the row is attached but not yet dynamically matched to the full spectrum.
proof idea
Definitional structure literal. Each field of the dataset-attachment record is filled by a concrete string or real constant: sector and dataset name the PTA channel, units fix the spectral-index scale, sensitivity is $0.80$, rsTargetScale is $0.481$, and currentlySensitive is false. No lemmas, tactics, or obligations.
why it matters
Supplies the §7 PTA row that the EPTA/PTA likelihood layer reads as its structural target. Downstream, the RS target is defined by projecting this row's target scale; status theorems assert positive sensitivity, positive target scale, and the explicit not-currently-sensitive flag; residual and interval comparisons (target below the EPTA $\gamma$ window, naive residual larger than half-width) unfold this attachment and reduce by norm_num. The one-statement PTA likelihood certificate and the module-level falsifier-dataset register certificate both consume it.
In the Recognition framework this is bookkeeping for a φ-ladder spectral signature against the nanohertz stochastic background, not a claim that PTA data confirm RS. It keeps the register honest: the channel is named, the $\log\varphi$ target is fixed, and current sensitivity is flagged false until a full dynamical match exists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.