nanograv_residual_lt_half_width
plain-language theorem explainer
The RS PTA running-index target sits closer to the NANOGrav 95% midpoint than the interval half-width. Anyone citing the NANOGrav likelihood certificate or the one-statement PTA attachment uses this bound. The proof is a pure numerical check after unfolding the fixed interval endpoints, midpoint, residual, and half-width.
Claim. Let $\beta_{\mathrm{lo}}=-0.80$, $\beta_{\mathrm{hi}}=2.96$ be the reported NANOGrav 15-year 95% credible endpoints for the running parameter, $m=(\beta_{\mathrm{lo}}+\beta_{\mathrm{hi}})/2$ the midpoint, $w=(\beta_{\mathrm{hi}}-\beta_{\mathrm{lo}})/2$ the half-width, and $t=\log\varphi$ the RS structural target. The residual $r=|m-t|$ satisfies $r<w$.
background
This module attaches a dataset-specific likelihood-style certificate to the §7 PTA stochastic-GW falsifier row. NANOGrav 15-year running spectral-index analysis reports a broad 95% credible interval $\beta\in[-0.80,2.96]$, consistent with zero. The RS structural target is $\log\varphi\approx 0.481$, stored on the falsifier-register PTA attachment as the native scale.
Sibling constants fix the arithmetic: lower and upper 95% endpoints, their midpoint, the half-width, the RS target, and the residual of the target from the midpoint. The certificate is deliberately a consistency and non-sensitivity test, not empirical confirmation: the interval is wide enough that the target lies inside it without the data being able to resolve the RS scale.
Related width and half constructions appear elsewhere in the stack (rational interval width, ratio-orbit half), but here the quantities are concrete real constants for this dataset row.
proof idea
Term-mode proof by unfolding. Expand the residual, midpoint, half-width, lower and upper 95% endpoints, RS target, and the PTA attachment handle to their numeric definitions, then discharge the strict inequality by norm_num. No lemmas beyond definitional unfolding; the claim is a closed real-arithmetic fact on fixed decimals.
why it matters
Feeds the NANOGrav PTA likelihood certificate structure, which packages positivity of half-width and target, target-inside-interval, this residual bound, and the not-currently-sensitive flag. Also appears in the one-statement PTA attachment theorem that conjoins interval membership, residual $<$ half-width, target $<$ half-width, and currentlySensitive = false.
Together these facts upgrade the falsifier-register PTA row from a bare handle to a proved consistency/non-sensitivity certificate: the RS target (tied to $\varphi$ from the forcing chain) sits inside the reported band, yet the band is still broader than the target scale itself. That honesty clause keeps the row marked not currently sensitive. Zero sorry and no new RS axioms; closure dated 2026-05-22 in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.