eptaGammaHalfWidth
plain-language theorem explainer
Defines the half-width of the recorded EPTA DR2 spectral-index interval as half the gap between the upper and lower bounds. Verification and PTA-attachment proofs cite it when comparing the naive residual of the RS structural scale against the observational window. The body is pure arithmetic on the two endpoint constants.
Claim. The half-width of the EPTA DR2 $\gamma$ interval is $(\gamma_{\mathrm{upper}}-\gamma_{\mathrm{lower}})/2$, where the endpoints are the recorded approximate bounds of the stochastic-background spectral index.
background
The module attaches an EPTA DR2 scalar record to the §7 PTA stochastic-GW falsifier row. EPTA reports a spectral index near $\gamma\approx 3.83$ with approximate asymmetric uncertainty $+0.82/-0.72$, recorded as an interval roughly $\gamma\in(3.11,4.65)$. The lower and upper endpoints are fixed real constants in this file; the half-width is their midpoint gap.
The RS structural PTA scale is $\log\varphi\approx 0.481$, stored on the shared PTA attachment record. Module scope stresses that EPTA's $\gamma$ is not NANOGrav's running index $\beta$ and is not identified with $\log\varphi$. The attachment is dataset accounting and scope control, not empirical confirmation of a derived RS spectral index.
proof idea
Definitional abbreviation: unfold to $(\mathrm{upper}-\mathrm{lower})/2$. No lemmas, tactics, or hypotheses. Downstream positivity and residual comparisons simply unfold this name with the two endpoints and finish by norm_num.
why it matters
Supplies the width scale used by eptaGammaHalfWidth_pos and by the residual inequality that the naive distance from the interval center to the RS target exceeds this half-width. That residual fact is conjoined in the one-statement EPTA PTA likelihood theorem and in the certificate structure, which records a positive interval, a positive RS target below the interval, and currentlySensitive = false.
In the Recognition verification layer this is the explicit numerical witness that a naive magnitude match of $\log\varphi$ into the EPTA $\gamma$ window fails. The module treats that failure as non-falsifying because the dynamic RS PTA spectral-index derivation is not yet formalized; the half-width keeps that scope claim machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.