epta_dataset_attachment_status
plain-language theorem explainer
The PTA stochastic-background dataset attachment has positive numerical sensitivity, a positive RS target scale, and is flagged as not currently sensitive. Verification authors cite it when assembling the EPTA DR2 likelihood certificate. The proof is a three-field term constructor from two positivity lemmas and reflexivity on the sensitivity flag.
Claim. The PTA stochastic gravitational-wave dataset attachment $D$ satisfies $0 < D.\mathrm{sensitivity}$, $0 < D.\mathrm{rsTargetScale}$, and $D$ is marked not currently sensitive.
background
This module records an EPTA DR2 scalar attachment on the §7 PTA stochastic-GW falsifier row. It is a structural, zero-sorry accounting theorem: EPTA reports a spectral index near $\gamma \approx 3.83$ with interval roughly $(3.11, 4.65)$, while the RS structural placeholder is $\log\varphi \approx 0.481$. Those quantities are deliberately not identified as the same physical parameter.
A DatasetAttachment carries sector, dataset handle, units, a numerical sensitivity, and an RS target scale. HasPositiveSensitivity means $0 < D.\mathrm{sensitivity}$; HasPositiveTargetScale means $0 < D.\mathrm{rsTargetScale}$. The shared PTA row ptaAttachment sets sensitivity $0.80$ and target scale $0.481$ (NANOGrav 15-year plus EPTA DR2 nanohertz background), and is documented as attached but not yet dynamically matched to the full spectrum.
Upstream lemmas pta_sensitivity_pos and pta_target_pos discharge the two positivity predicates on that row by unfolding and norm_num.
proof idea
Term-mode triple constructor. The first conjunct is exactly pta_sensitivity_pos (unfolds HasPositiveSensitivity on ptaAttachment and closes $0 < 0.80$ by norm_num). The second is pta_target_pos (same pattern for $0 < 0.481$). The third is rfl on the boolean field currentlySensitive = false as recorded in the attachment. No further rewriting or case analysis.
why it matters
Feeds the master certificate eptaPTALikelihoodCert as its dataset_status field, alongside interval positivity, target positivity, target-below-interval, and naive-residual comparisons. That cert is the module's closure object for EPTA DR2 PTA likelihood attachment.
In the Recognition verification stack this is scope control, not a physics claim: it registers that the PTA row is present with positive scales and explicitly not currently sensitive, matching the module status note that a naive magnitude comparison does not place $\log\varphi$ inside the EPTA $\gamma$ interval and that this is not an RS falsification because the dynamic RS PTA spectral-index derivation is not yet formalized. It sits on the falsifier-register side of the framework rather than on the T0–T8 forcing chain, and keeps the PTA stochastic-background sector honest until a full spectral match exists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.