nanogravBetaMidpoint
plain-language theorem explainer
Defines the midpoint of the NANOGrav 15-year 95% credible interval on the PTA running spectral index β. Anyone building the likelihood-style residual against the RS target log φ cites this constant. It is a one-line arithmetic average of the reported lower and upper bounds.
Claim. Let $\beta_{\mathrm{lo}}$ and $\beta_{\mathrm{hi}}$ be the lower and upper endpoints of the NANOGrav 15-year 95% credible interval on the PTA running parameter $\beta$. The midpoint is $\beta_{\mathrm{mid}} := (\beta_{\mathrm{lo}} + \beta_{\mathrm{hi}})/2 \in \mathbb{R}$.
background
The 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 for β consistent with zero, approximately β ∈ [-0.80, 2.96]. The RS structural target is log φ ≈ 0.481, stored on the falsifier-register PTA attachment as the rsTargetScale.
This midpoint is not a physical prediction. It is only the center of the reported interval, so that a residual |midpoint − RS target| can be compared to the interval half-width. The certificate is a consistency / non-sensitivity test: the target must lie inside the interval, yet the interval is still too wide to confirm RS.
Sibling constants fix the lower and upper 95% endpoints and the half-width; the RS target is the separate positive scale log φ.
proof idea
Pure definition: arithmetic mean of the two endpoint constants. No lemmas, no tactics, no unfolding beyond the two bound defs. Downstream residual and comparison theorems unfold this name and discharge the resulting numeric inequalities by norm_num.
why it matters
Feeds the residual |midpoint − RS target| and the theorem that this residual is strictly smaller than the 95% half-width. Those facts close the structural certificate: the RS target sits inside the NANOGrav interval, while the half-width still dominates the target, so the dataset row stays marked not currently sensitive.
In the Recognition framework this is verification plumbing, not a forcing-chain step. It records that the PTA running index has not yet resolved the log-φ scale that appears in RS mass and coupling ladders. Parent uses are the residual def and the residual-versus-half-width inequality in the same module; together they upgrade the falsifier register without claiming empirical confirmation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.