eptaGammaHalfWidth_pos
plain-language theorem explainer
The recorded EPTA DR2 spectral-index half-width is strictly positive. Anyone wiring the EPTA interval into the §7 PTA falsifier row needs this before residual or containment comparisons. The proof unfolds the half-width to the numerical endpoints and finishes by norm_num.
Claim. The half-width proxy of the recorded EPTA DR2 spectral-index interval is positive: $0 < (\gamma_{\mathrm{U}} - \gamma_{\mathrm{L}})/2$, where the lower endpoint is $\gamma_{\mathrm{L}} = 3.11$ and the upper endpoint is $\gamma_{\mathrm{U}} = 4.65$.
background
This module is a dataset-accounting attachment for EPTA DR2 on 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 endpoints $3.11$ and $4.65$.
The half-width proxy is defined as half the difference of those endpoints. It is a pure numerical bookkeeping quantity used to state positivity of the recorded interval and to compare naive residuals against that width. The RS structural PTA scale $\log\varphi \approx 0.481$ lives in the shared falsifier-register attachment; the module explicitly warns that EPTA's $\gamma$ is not NANOGrav's $\beta$ and is not identified with $\log\varphi$.
proof idea
Term-mode proof by unfolding. Expand the half-width definition to $(\mathrm{upper}-\mathrm{lower})/2$, then expand the two endpoint constants $4.65$ and $3.11$. The resulting concrete rational inequality is discharged by norm_num. No lemmas beyond the three local defs are required.
why it matters
Part of the structural EPTA DR2 attachment cert (module status: 0 sorry, 0 new RS axioms). The module's two certified facts are (1) the EPTA $\gamma$ interval is positive, matching the sign of the RS PTA structural signature, and (2) a naive magnitude check does not place $\log\varphi$ inside that interval. This positivity lemma is the elementary width step behind (1).
It is scope control, not empirical confirmation: the dynamic RS PTA spectral-index derivation is not yet formalized, so mismatch with $\log\varphi$ is not an RS falsification. No downstream dependents are recorded yet; the lemma sits with the sibling interval and residual facts that close the attachment row.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.