eptaRSTarget
plain-language theorem explainer
Aliases the Recognition Science structural PTA target scale as a real constant equal to the §7 dataset attachment value (log φ ≈ 0.481). Anyone comparing EPTA DR2 spectral-index data to the RS PTA placeholder cites this binding. The body is a one-line projection of the attachment record's target field.
Claim. Define the RS structural PTA target scale $T_{\mathrm{RS}} \in \mathbb{R}$ by $T_{\mathrm{RS}} := s$, where $s$ is the target scale stored on the §7 PTA dataset attachment (numerically $\log\varphi \approx 0.481$).
background
The module attaches an EPTA DR2 scalar record to the §7 PTA stochastic-GW falsifier row. EPTA reports a stochastic-background spectral index near $\gamma \approx 3.83$ with approximate interval $\gamma \in (3.11, 4.65)$. Separately, Recognition Science records a structural PTA target scale $\log\varphi \approx 0.481$ on the shared PTA attachment object.
That attachment is the single source of truth for the RS-side number used in this verification layer. The module header stresses that EPTA's $\gamma$ is not the same physical parameter as NANOGrav's running index $\beta$, and is not identified with the structural placeholder $\log\varphi$. The present definition simply names that placeholder for local use in residual and interval comparisons.
This is dataset accounting and scope control, not an empirical confirmation claim. The module is closed with zero sorry and no new RS-specific axioms.
proof idea
Definitional one-liner: unfold the name to the real field rsTargetScale on the shared PTA attachment record. No tactics, no lemmas, no arithmetic. Downstream positivity and ordering proofs re-unfold this alias together with the attachment and discharge the resulting decimal inequalities by norm_num.
why it matters
Gives a stable local name for the RS PTA structural scale so the EPTA likelihood layer can state sign compatibility and honest non-match without re-quoting the attachment each time. Downstream, the naive residual is $|\gamma_{\mathrm{central}} - T_{\mathrm{RS}}|$; theorems prove $T_{\mathrm{RS}} > 0$, $T_{\mathrm{RS}}$ lies strictly below the EPTA $\gamma$ lower edge, and that residual exceeds the half-width of the reported interval.
Those facts feed the certificate structure and the one-statement attachment theorem, which also record that the attachment is marked not currently sensitive. The module is explicit: a naive magnitude mismatch is scope control, not falsification, because the dynamic RS PTA spectral-index derivation is not yet formalized. In the broader RS picture this sits in verification against PTA stochastic-GW data, using the forced $\varphi$ scale rather than a free fit parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.