EPTAPTALikelihoodCert
plain-language theorem explainer
Certificate packing five EPTA DR2 PTA accounting facts: the reported spectral-index 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 PTA attachment has positive sensitivity and scale but is marked not currently sensitive. Falsifier-register and verification authors cite it when wiring the likelihood row. The structure is a pure Prop bundle; inhabitance is discharged by sibling lemmas.
Claim. A certificate of five propositions on the EPTA DR2 PTA record: the reported spectral-index interval satisfies $0 < \gamma_{\mathrm{lo}} < \gamma_{\mathrm{hi}}$; the RS structural PTA target $t$ obeys $0 < t$; $t$ lies strictly below the interval ($t < \gamma_{\mathrm{lo}}$); the interval half-width is strictly smaller than the naive residual $|\gamma_{\mathrm{c}} - t|$; and the PTA dataset attachment has positive sensitivity, positive target scale, and is marked 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 near $\gamma \approx 3.83$ with approximate asymmetric uncertainty $+0.82/-0.72$, recorded 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 RS structural PTA target $t$ is the dataset attachment's rsTargetScale, equal to $\log\varphi \approx 0.481$. The naive residual is $|\gamma_{\mathrm{c}}-t|$.
Positive-sensitivity and positive-target-scale are the standard dataset predicates $0 < D.\mathrm{sensitivity}$ and $0 < D.\mathrm{targetScale}$. The module status is structural (zero sorry, zero new RS axioms): a dataset-accounting and scope-control record, not empirical confirmation. EPTA's $\gamma$ is not NANOGrav's running index $\beta$ and is not the RS placeholder $\log\varphi$.
proof idea
No proof body: this is a structure whose fields are propositions. Inhabitance is supplied downstream by the concrete witness that assigns each field to a sibling lemma: interval positivity from the numerical lower/upper bounds, target positivity from the attachment scale, target-below-interval from comparing $\log\varphi$ to $3.11$, residual-versus-half-width from the absolute deviation at the central $\gamma$, and dataset status from the positive-sensitivity/target lemmas plus reflexivity on the currentlySensitive = false flag.
why it matters
This is the master cert type for the EPTA PTA likelihood attachment. The concrete witness and the Nonempty theorem inhabit it; the one-statement theorem flattens the five fields into a single conjunction for register consumers. Downstream, the aggregate falsifier likelihood register includes a Nonempty slot for this cert alongside Planck $\Omega_\Lambda$, Cassini, and other rows.
In the Recognition framework it enforces scope control on the §7 PTA stochastic-GW falsifier: it records that a naive magnitude comparison does not place $\log\varphi$ inside the EPTA $\gamma$ band, while stressing that this is not an RS falsification because the dynamic RS PTA spectral-index derivation is not yet formalized. It keeps the positive-sign consistency of the structural target without overclaiming parameter identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.