eptaGammaUpper
plain-language theorem explainer
Records the upper endpoint 4.65 of the EPTA DR2 stochastic-background spectral-index interval γ ∈ (3.11, 4.65), taken from the quoted +0.82 uncertainty on the central value ≈ 3.83. Dataset-accounting code and the EPTA PTA likelihood certificate cite it as the fixed right endpoint. The body is a bare real literal; no proof work.
Claim. Define the upper endpoint of the EPTA DR2 spectral-index interval by $\gamma_{\mathrm{upper}} := 4.65$, corresponding to the quoted approximate $+0.82$ uncertainty on the reported central value $\gamma \approx 3.83$.
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 approximate asymmetric errors $+0.82/-0.72$, which the module freezes as the open interval $\gamma \in (3.11, 4.65)$. The companion constants are the lower endpoint $3.11$ and the central value used for residual comparisons.
The RS structural PTA target in this register is $\log\varphi \approx 0.481$ (from the falsifier-register dataset attachment), not a claim that EPTA's $\gamma$ equals that scale. Module scope is explicit: EPTA $\gamma$ is neither NANOGrav's running index $\beta$ nor the RS placeholder $\log\varphi$. The attachment is dataset accounting and scope control, not empirical confirmation of a derived RS spectral index.
Interval width utilities elsewhere in the stack (rational interval width as high minus low) motivate the half-width proxy built from this upper endpoint and its lower sibling.
proof idea
Definitional constant: the real literal $4.65$ is assigned directly. No tactics, lemmas, or algebraic reduction. Downstream proofs that mention the upper endpoint simply unfold this name and discharge numeric goals with norm_num.
why it matters
Pins the right edge of the EPTA $\gamma$ interval used throughout the likelihood attachment. Half-width is $(4.65-3.11)/2$; positivity of the interval, the half-width positivity lemma, and the naive-residual-versus-half-width comparison all unfold this constant. The certificate structure EPTAPTALikelihoodCert and the one-statement theorem package those facts: the EPTA interval is positive (sign-consistent with a positive RS PTA signature), yet a naive magnitude comparison does not place $\log\varphi$ inside the interval, and the attachment is marked not currently sensitive.
That second fact is intentional scope control. The dynamic RS PTA spectral-index derivation is not yet formalized, so mismatch with $\log\varphi$ is not an RS falsification. The declaration therefore supports verification bookkeeping on the PTA falsifier row rather than a forcing-chain landmark (T0–T8) or a mass/alpha claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.