epta_rs_target_below_gamma_interval
plain-language theorem explainer
The RS structural PTA target (log φ) lies strictly below the lower edge of the EPTA DR2 γ interval. Dataset-accounting and PTA-falsifier work cites this to record that a naive magnitude match fails. It is scope control, not a physics falsification. The proof unfolds the three numeric defs and closes by norm_num.
Claim. The Recognition Science structural target scale $\log\varphi$ is strictly smaller than the lower endpoint of the recorded EPTA DR2 spectral-index interval: $\mathrm{rsTargetScale} < \gamma_{\mathrm{lower}}$.
background
This 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 asymmetric errors $+0.82/-0.72$, so the recorded interval is roughly $\gamma\in(3.11,4.65)$. The lower endpoint used here is that recorded lower bound.
The RS structural placeholder is $\log\varphi\approx 0.481$, stored on the PTA attachment record as the structural target scale. Module scope is explicit: EPTA's $\gamma$ is not NANOGrav's running index $\beta$, and it is not the same physical parameter as the RS placeholder $\log\varphi$. The dynamic RS PTA spectral-index derivation is not yet formalized.
Sibling facts in the same file establish positivity of the $\gamma$ interval and of the RS target, and that the naive residual exceeds the half-width. Together they form a dataset-accounting certificate, not an empirical confirmation.
proof idea
Term-mode proof. Unfold the three concrete definitions (RS target scale from the PTA attachment record, and the EPTA $\gamma$ lower endpoint), then discharge the strict inequality by norm_num on the resulting rationals/reals. No lemmas beyond definitional unfolding; pure numeric comparison.
why it matters
Fills the scope-control slot in the EPTA PTA likelihood certificate: the cert bundles interval positivity, target positivity, this below-interval fact, the naive-residual-versus-half-width comparison, and the dataset attachment status. The one-statement theorem packages the same conjunction for a single citation.
In the Recognition framework this sits on the verification side of the PTA stochastic-GW falsifier row. It records that a naive magnitude comparison of $\log\varphi$ against EPTA $\gamma$ fails, while insisting that failure is not an RS falsification until the dynamic spectral-index derivation exists. Zero sorry, zero new RS axioms; pure accounting closure for the 2026-05-22 structural theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.