epta_pta_likelihood_one_statement
plain-language theorem explainer
Packages the EPTA DR2 PTA attachment into one conjunction: the reported γ-interval is positive and ordered, the RS structural target log φ is positive and lies strictly below that interval, the naive residual exceeds the half-width, and the dataset is marked not currently sensitive, with a nonempty certificate. Verification authors cite it as the single entry point for the EPTA row. The proof is a six-component term pairing prior positivity lemmas with rfl and the inhabited cert.
Claim. The EPTA $\gamma$-interval satisfies $0 < \gamma_{\mathrm{lo}} < \gamma_{\mathrm{hi}}$, the RS structural PTA target $t$ obeys $0 < t$ and $t < \gamma_{\mathrm{lo}}$, the half-width of the interval is strictly smaller than the naive residual $|\gamma_{\mathrm{c}} - t|$, the PTA attachment flag $\mathrm{currentlySensitive}$ is false, and the EPTA PTA likelihood certificate type is inhabited.
background
This module records an EPTA DR2 scalar on the §7 PTA stochastic-GW falsifier row. EPTA reports a stochastic-background spectral index near $\gamma \approx 3.83$ with approximate asymmetric errors $+0.82/-0.72$, encoded here as the open interval $(\gamma_{\mathrm{lo}},\gamma_{\mathrm{hi}}) = (3.11, 4.65)$. The half-width proxy is $(\gamma_{\mathrm{hi}}-\gamma_{\mathrm{lo}})/2$; the naive residual is the absolute gap between the central $\gamma$ and the RS structural target.
The RS structural PTA target is the placeholder scale $\log\varphi \approx 0.481$ taken from the shared falsifier-register attachment ptaAttachment.rsTargetScale. Module scope is explicit: EPTA's $\gamma$ is not NANOGrav's running index $\beta$, and it is not identified with $\log\varphi$. The certificate therefore only asserts sign-level positivity of the interval and target, plus a magnitude comparison showing $\log\varphi$ is not inside the EPTA band under a naive reading.
Upstream lemmas already discharge the numeric facts by norm_num after unfolding the endpoint defs: the interval is positive and ordered, the target is positive and strictly below $\gamma_{\mathrm{lo}}$, and the residual exceeds the half-width.
proof idea
Term-mode six-tuple. The first four conjuncts are the named lemmas epta_gamma_interval_positive, eptaRSTarget_pos, epta_rs_target_below_gamma_interval, and epta_naive_residual_gt_half_width (each a short unfold + norm_num proof on the concrete reals). The fifth conjunct is rfl on ptaAttachment.currentlySensitive = false. The sixth is eptaPTALikelihoodCert_inhabited, which supplies a witness of the certificate structure bundling those same facts with the dataset-status fields.
why it matters
Closes the EPTA DR2 likelihood-attachment row as a structural theorem: zero sorry, zero new RS-internal axioms, dated closure 2026-05-22. It is the one-statement surface for the module's certificate EPTAPTALikelihoodCert, which packages interval positivity, target positivity, target-below-interval, residual-vs-half-width, and the explicit not-currently-sensitive flag.
In the Recognition verification stack this is dataset accounting and scope control, not empirical confirmation of the PTA spectral law. The module doc stresses that a naive magnitude mismatch between $\log\varphi$ and EPTA $\gamma$ is not an RS falsification, because the dynamic RS PTA spectral-index derivation is not yet formalized. No downstream consumers are wired yet (used_by empty); the declaration exists so later falsifier-register aggregation can import a single proved bundle rather than reassemble the numeric lemmas.
Framework contact is limited to the shared PTA attachment target scale (the structural $\log\varphi$ placeholder). It does not touch the forcing chain T0–T8, RCL, or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.