eptaGammaCentral
plain-language theorem explainer
Records the EPTA DR2 central spectral index γ = 3.83 for the stochastic gravitational-wave background. Verification and PTA-falsifier work cites it as the fixed dataset anchor for residual and interval checks against the RS structural scale. It is a bare real constant, not a derived claim.
Claim. The EPTA DR2 representative central value of the stochastic-background spectral index is $\gamma_{\mathrm{EPTA}} = 3.83$.
background
The module attaches an EPTA DR2 scalar record to the §7 PTA stochastic-GW falsifier row. Published analyses quote a spectral index near $\gamma \approx 3.83$ with approximate asymmetric errors $+0.82/-0.72$, so the working interval is roughly $\gamma \in (3.11, 4.65)$.
Recognition Science keeps a separate structural PTA scale $\log\varphi \approx 0.481$ in the falsifier register. EPTA's $\gamma$ is not NANOGrav's running index $\beta$ and is not identified with $\log\varphi$. The module only certifies sign-level positivity of the EPTA interval and that a naive magnitude comparison does not place $\log\varphi$ inside that interval; the dynamical RS PTA spectral-index derivation is not yet formalized.
This constant is the fixed central anchor for those accounting checks. It is dataset bookkeeping and scope control, not empirical confirmation of RS.
proof idea
Definitional binding of a real literal: the symbol is set equal to $3.83$ with no lemmas, tactics, or algebraic reduction. Downstream residual and comparison theorems unfold this constant and discharge inequalities by norm_num.
why it matters
Supplies the numerator side of the naive residual $|\gamma_{\mathrm{central}} - \log\varphi|$ used by eptaNaiveResidual, and is unfolded in the theorem that this residual exceeds the recorded half-width. That theorem is the module's second structural fact: a direct magnitude match of the RS placeholder to EPTA $\gamma$ fails, which the module header treats as non-falsifying because the RS dynamical PTA index is still open.
Together with the lower/upper endpoints and half-width siblings, it closes the EPTA DR2 attachment as a zero-sorry, zero-new-axiom dataset record on the PTA falsifier row. It does not advance T0–T8 forcing, RCL, or mass-ladder claims; it only pins the external number those verification lemmas compare against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.