eptaGammaLower
plain-language theorem explainer
Records the lower endpoint 3.11 of the EPTA DR2 stochastic-background spectral-index interval γ, from the quoted central value ≈3.83 and −0.72 uncertainty. Downstream positivity, half-width, and likelihood-cert lemmas cite this constant as the left bound of γ ∈ (3.11, 4.65). The body is a bare real literal; no proof work.
Claim. The lower endpoint of the EPTA DR2 PTA spectral-index interval is the real number $3.11$, obtained from the reported central value $\gamma \approx 3.83$ and the quoted approximate lower uncertainty $-0.72$.
background
The module attaches an EPTA DR2 scalar record to the §7 PTA stochastic-GW falsifier row. EPTA analyses quote a stochastic-background spectral index near $\gamma \approx 3.83$ with asymmetric uncertainty roughly $+0.82/-0.72$, so the working interval is $\gamma \in (3.11, 4.65)$. This definition is the left endpoint of that interval.
The RS structural PTA target in the same module is $\log\varphi \approx 0.481$ (from the falsifier-register dataset attachment). EPTA's $\gamma$ is not NANOGrav's running index $\beta$ and is not identified with $\log\varphi$. The cert only checks sign-level positivity of the EPTA interval and that a naive magnitude comparison does not place $\log\varphi$ inside it; the dynamic RS PTA spectral-index derivation is not yet formalized.
Sibling constants fix the central value, upper endpoint $4.65$, half-width proxy, and the RS target scale used in residual comparisons.
proof idea
Definitional constant: the real literal $3.11$ is assigned directly. No tactics, lemmas, or algebraic reduction. Downstream theorems unfold this name and discharge numeric goals with norm_num.
why it matters
Anchors every numeric comparison in the EPTA PTA likelihood attachment. Half-width is $(eptaGammaUpper - eptaGammaLower)/2$; positivity of the interval is $0 < eptaGammaLower \wedge eptaGammaLower < eptaGammaUpper$; the cert structure requires the RS target below this lower bound; the one-statement theorem packages those facts with the residual-versus-half-width inequality and the currentlySensitive = false flag.
In the Recognition verification layer this is dataset accounting and scope control, not empirical confirmation of RS. It keeps the §7 PTA falsifier row honest: the EPTA $\gamma$ band is positive (consistent with a positive RS structural signature) while a naive placement of $\log\varphi$ inside that band fails, and that failure is explicitly not an RS falsification until the spectral-index derivation exists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.