epta_gamma_interval_positive
plain-language theorem explainer
EPTA DR2's recorded spectral-index window sits strictly above zero: the lower endpoint is positive and strictly less than the upper endpoint. Verification and PTA-attachment work cites this as the sign-level half of the EPTA likelihood certificate. The proof unfolds the two numeric bounds and discharges the inequalities by `norm_num`.
Claim. The recorded EPTA DR2 spectral-index interval satisfies $0 < \gamma_{\mathrm{lower}}$ and $\gamma_{\mathrm{lower}} < \gamma_{\mathrm{upper}}$ (with the approximate window $\gamma \in (3.11, 4.65)$).
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 as the open interval $(\gamma_{\mathrm{lower}}, \gamma_{\mathrm{upper}}) \approx (3.11, 4.65)$.
The RS structural PTA placeholder in the same register is $\log\varphi \approx 0.481$ (from ptaAttachment.rsTargetScale). Module scope is explicit: EPTA's $\gamma$ is not NANOGrav's running index $\beta$, and is not identified with $\log\varphi$. The certificate therefore only records sign consistency and a naive-magnitude non-match; it is dataset accounting, not empirical confirmation of a derived RS PTA spectrum.
Sibling constants fix the numeric endpoints, half-width, RS target, and residual used by the full attachment certificate.
proof idea
One-line numeric check. Unfold the definitions of the lower and upper EPTA $\gamma$ endpoints to their concrete rational (or decimal) values, then apply norm_num to prove both $0 < \gamma_{\mathrm{lower}}$ and $\gamma_{\mathrm{lower}} < \gamma_{\mathrm{upper}}$. No lemmas beyond definitional unfolding are required.
why it matters
Feeds the EPTA PTA likelihood certificate structure as the interval_positive field, and appears as the first conjunct of the one-statement attachment theorem. Together with positivity of the RS target, the target-below-interval fact, and the residual-versus-half-width comparison, it closes the structural half of the EPTA DR2 row: the observed window is positive (matching the sign of the RS PTA signature) while a naive magnitude comparison of $\log\varphi$ against that window fails by design.
That failure is scope control, not falsification: the dynamic RS PTA spectral-index derivation is not yet formalized, so placing $\log\varphi$ inside EPTA's $\gamma$ band is not a claim the framework currently makes. The module status is structural theorem (zero sorry, zero new RS axioms). Landmark contact is only the RS target scale $\log\varphi$ from the forcing chain's golden ratio $\varphi$; no T0–T8 step is proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.