eptaPTALikelihoodCert
plain-language theorem explainer
Packages the EPTA DR2 PTA spectral-index attachment into one certificate: the reported γ interval is positive, the RS structural target log φ is positive and lies strictly below that interval, the naive residual exceeds the half-width, and the dataset is present but marked not currently sensitive. Verification authors cite it when assembling the §7 PTA falsifier row. The definition is a pure structure constructor wiring five already-proved numeric and status lemmas.
Claim. The EPTA PTA likelihood certificate is the record asserting $0 < \gamma_{\mathrm{lower}} < \gamma_{\mathrm{upper}}$, that the RS structural target $t=\log\varphi$ satisfies $0<t$ and $t<\gamma_{\mathrm{lower}}$, that the EPTA half-width is strictly smaller than the naive residual $|\gamma_{\mathrm{central}}-t|$, and that the PTA dataset attachment has positive sensitivity, positive target scale, and is flagged not currently sensitive.
background
This module attaches an EPTA DR2 scalar record to the §7 PTA stochastic-GW falsifier row. EPTA reports a stochastic-background spectral index around $\gamma\approx 3.83$ with approximate asymmetric uncertainty, recorded as the interval $\gamma\in(3.11,4.65)$. The RS structural target is $\log\varphi\approx 0.481$, stored on the PTA attachment as the target scale.
EPTA's $\gamma$ is not NANOGrav's running index $\beta$ and is not the same physical parameter as the RS placeholder $\log\varphi$. Upstream lemmas therefore only lock sign compatibility and an honest non-match: the $\gamma$ interval is positive (by norm_num on the recorded bounds), the RS target is positive and strictly below the lower endpoint, the naive residual exceeds the half-width, and the attachment status triple holds (positive sensitivity, positive target scale, currentlySensitive = false). The module is dataset-accounting and scope control, not empirical confirmation.
proof idea
Pure structure constructor. Each field of the certificate is filled by a sibling lemma already proved upstream: positivity of the recorded $\gamma$ bounds, positivity of the RS target, the strict inequality placing the target below the lower endpoint, the residual-versus-half-width comparison, and the packaged attachment-status conjunction. Those lemmas themselves unfold the numeric constants and discharge by norm_num (or by reflexivity on the sensitivity flag). No new arithmetic or case analysis occurs here.
why it matters
Supplies the witness for the inhabitedness theorem that Nonempty holds for the certificate type, which supports the one-statement EPTA PTA likelihood attachment result in the same module. In the Recognition verification stack this locks the §7 PTA falsifier-row accounting: the certificate records that a naive magnitude comparison of $\log\varphi$ against EPTA $\gamma$ fails, and explicitly marks the attachment not currently sensitive, so the mismatch is scope control rather than an RS falsification. The dynamic RS PTA spectral-index derivation remains unformalized; this definition closes the structural record with zero sorry and zero new RS-specific axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.