nanogravRSTarget
plain-language theorem explainer
The RS structural target on the NANOGrav PTA spectral-index scale is the fixed real 0.481, i.e. log φ from the §7 falsifier-register PTA attachment. Consistency and non-sensitivity certificates for the NANOGrav 15-year β interval cite this constant as the RS prediction. The definition is a one-line alias of the attachment field rsTargetScale, not a derived computation.
Claim. Define the RS structural PTA target scale to be the real number $0.481$, equal to $\log\varphi$ as recorded on the PTA stochastic gravitational-wave background dataset attachment (spectral-index units).
background
This module attaches a likelihood-style certificate to the NANOGrav 15-year PTA stochastic-background row. The reported 95% credible interval for the running spectral parameter is the broad band $\beta \in [-0.80, 2.96]$, consistent with zero and with the SMBHB reference slope $\gamma = 13/3$.
The falsifier-register PTA attachment records sector, dataset handle, units (spectral-index scale), a sensitivity figure $0.80$, and an RS structural target scale $0.481$. That target is the positive $\varphi$-rational signature $\log\varphi$, not a full dynamical spectrum match. The module status is structural: zero sorry, zero new RS-internal axioms; a consistency / non-sensitivity test, not empirical confirmation.
Sibling constants unpack the same interval: lower/upper 95% edges, midpoint, and half-width. Residuals and containment statements are measured against the target defined here.
proof idea
Pure definitional alias: the real is definitionally equal to the rsTargetScale field of the PTA dataset attachment record. No tactics, no lemmas, no arithmetic. Downstream proofs that need the numeric value unfold this name together with the attachment and discharge inequalities by norm_num.
why it matters
This constant is the RS side of every NANOGrav PTA comparison in the module. It appears in the residual (absolute deviation from the interval midpoint), the containment theorem (target inside $[-0.80, 2.96]$), the residual-versus-half-width bound, and the half-width-greater-than-target non-sensitivity fact. The certificate structure packages positivity of the half-width and of this target with interval membership; the one-statement theorem conjoins those facts with the register flag that the row is not currently sensitive.
In the broader framework the value is the $\varphi$-ladder landmark $\log\varphi$ (forced self-similar scale from the T5–T6 forcing chain), used here only as a structural spectral-index scale, not as a mass or coupling prediction. The honest scientific claim is consistency plus non-sensitivity: the target sits inside a still-too-wide band, so the PTA row remains an open falsifier attachment rather than a confirmation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.