eptaNaiveResidual
plain-language theorem explainer
Absolute difference between EPTA DR2's central spectral index (γ ≈ 3.83) and the RS structural PTA target (log φ ≈ 0.481). Verification authors cite it when proving that a naive magnitude match fails: the residual exceeds the quoted half-width. One-line absolute-value definition of two recorded scalars.
Claim. The naive residual is $|\gamma_{\mathrm{EPTA}} - \log\varphi|$, where $\gamma_{\mathrm{EPTA}} = 3.83$ is the EPTA DR2 central spectral index and $\log\varphi$ is the RS structural PTA target scale from the §7 dataset attachment.
background
This module attaches an EPTA DR2 scalar record to the §7 PTA stochastic-GW falsifier row. EPTA reports a stochastic-background spectral index around γ ≈ 3.83 with approximate asymmetric uncertainty +0.82/−0.72, so the recorded interval is roughly γ ∈ (3.11, 4.65). The RS structural target is log φ ≈ 0.481, stored as the PTA attachment's target scale.
The two inputs are the EPTA central value 3.83 and that RS target scale. The module stresses that EPTA's γ is not the same physical parameter as NANOGrav's running index β, and is not the same as the structural placeholder log φ. The residual is therefore a bookkeeping distance, not a likelihood score.
Scope is dataset accounting and scope control: the cert proves positivity of the EPTA interval and that a naive magnitude comparison does not place log φ inside it. That mismatch is not an RS falsification, because the dynamic RS PTA spectral-index derivation is not yet formalized.
proof idea
Pure definition: unfold to the absolute value of the difference of the two named scalars (EPTA central γ and the RS PTA target scale). No lemmas, no tactics.
why it matters
Feeds the inequality that the residual exceeds the EPTA half-width, which is one conjunct of the one-statement EPTA PTA likelihood attachment theorem and of the certificate structure (interval positive, target positive, target below the γ interval, residual larger than half-width, attachment marked not currently sensitive).
In the Recognition verification layer this is the explicit magnitude gap that justifies marking the EPTA row as present and positive but not currently sensitive. It keeps the §7 PTA falsifier honest: sign-level consistency holds, while a naive γ-versus-log-φ comparison is recorded as a non-match rather than claimed confirmation. Touches the open gap that a full dynamic RS PTA spectral-index derivation is still missing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.