eptaRSTarget_pos

The module attaches an EPTA DR2 scalar record to the PTA stochastic-GW falsifier row. EPTA reports a spectral index near $\gamma\approx 3.83$ with an approximate interval $\gamma\in(3.11,4.65)$. Separately, the RS structural PTA placeholder is $\log\varphi\approx 0.481$, stored as the attachment field rsTargetScale and exposed here as the scalar target.

That target is not the same physical parameter as EPTA's $\gamma$ (nor as NANOGrav's running index $\beta$). The module therefore only records sign compatibility and an honest non-match under naive magnitude comparison; it is dataset accounting and scope control, not empirical confirmation.

Sibling constants fix the EPTA interval bounds, half-width, and the naive residual between the RS target and the EPTA central value. Positivity of the RS target is the elementary sign fact needed before those comparisons.

Term-style tactic proof. Unfold the target definition and the PTA attachment record so the goal becomes a concrete numerical inequality on the recorded scale. Close with norm_num. No external lemmas are required beyond definitional unfolding.

Feeds the EPTA PTA likelihood certificate as the target_pos field, and appears explicitly in the one-statement attachment theorem as the conjunct $0 < t_{\mathrm{RS}}$. Together with interval positivity, target-below-interval, and residual-versus-half-width, it completes the structural checklist for this falsifier row.

In the broader Recognition framework the target scale is $\log\varphi$, forced upstream by the self-similar fixed point (T6) after J-uniqueness (T5). The cert deliberately stops short of claiming a spectral-index derivation: the dynamic RS PTA index is not yet formalized, so a naive mismatch with EPTA's $\gamma$ is recorded as non-sensitive rather than as a falsification. This lemma is the sign half of that honest bookkeeping.