module module moderate

`IndisputableMonolith.Verification.NANOGravPTALikelihood`

Encodes the NANOGrav PTA 95% interval on the GW-background spectral index β, the RS target, and the residual, then proves the target lies inside the interval. Verification authors cite it when wiring PTA data into the quantum-gravity falsifier register. Content is named numeric constants plus elementary interval and positivity lemmas.

claimLet $\beta_{\mathrm{lo}}^{95}$ and $\beta_{\mathrm{hi}}^{95}$ be the reported broad NANOGrav 95% bounds on the PTA spectral index $\beta$, with midpoint $m$ and half-width $w>0$. Let $\beta_{\mathrm{RS}}>0$ be the Recognition Science target and $r=|\beta_{\mathrm{RS}}-m|$ the residual. The module records these values and establishes $\beta_{\mathrm{RS}}\in[\beta_{\mathrm{lo}}^{95},\beta_{\mathrm{hi}}^{95}]$, equivalently $r<w$, and $w>\beta_{\mathrm{RS}}$ where stated, plus a dataset-attachment status flag.

background

NANOGrav's pulsar-timing array constrains the nanohertz stochastic gravitational-wave background. The usual power-law parametrization uses a spectral index β; the collaboration quotes a broad 95% interval on β. This module freezes that reported interval as named constants (lower/upper endpoints, midpoint, half-width) so later falsifier machinery can treat the data as a fixed numeric attachment rather than free parameters.

Recognition Science supplies a definite target β_RS on the same observable. The residual is the absolute deviation of that target from the interval midpoint. Upstream, FalsifierRegisterDatasets attaches concrete named datasets and sensitivity records to every row of the quantum-gravity master plan §7 falsifier register; this file is the NANOGrav PTA row of that attachment layer.

Sibling declarations also expose positivity of the half-width and of the RS target, and a status flag recording that the dataset is attached.

proof idea

Definition layer: six numeric defs fix the 95% endpoints, midpoint, half-width, RS target, and residual. Lemma layer: positivity of the half-width and of the RS target are immediate from the concrete values; membership of the target in the closed 95% interval, residual strictly below half-width, and half-width exceeding the RS target are closed interval-arithmetic comparisons on those constants. A final status declaration records dataset attachment. No analytic derivation of β_RS lives here; the module only certifies the numeric fit against the published PTA band.

why it matters in Recognition Science

Feeds the parent module FalsifierLikelihoodRegister, which "aggregates Sessions 107--115: the dataset-specific likelihood/status layer over the quantum-gravity master plan §7 falsifier register." Without a pinned NANOGrav interval and a proved inside-band residual, that register cannot mark the PTA falsifier row as data-attached and currently non-falsifying.

In the broader RS verification stack this is an observational gate, not a forcing-chain step: T0--T8 fix J, φ, the eight-tick octave, and D=3; here those commitments are confronted with a real GW-background constraint. A future shift of the NANOGrav 95% band that excludes β_RS would flip the attachment status and surface as a register-level falsification signal.

scope and limits

Does not derive the RS β target from first principles; only consumes it as a numeric constant.
Does not re-analyze NANOGrav timing residuals or recompute the PTA likelihood.
Does not claim uniqueness of β among alternative GW-background models.
Does not update automatically if NANOGrav revises the published 95% interval.
Does not address Hellings-Downs angular correlations or other PTA systematics.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Verification.FalsifierLikelihoodRegister module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.FalsifierRegisterDatasets module_import

declarations in this module (16)

def nanogravBetaLower95 L46
def nanogravBetaUpper95 L49
def nanogravBetaMidpoint L52
def nanogravBetaHalfWidth95 L55
def nanogravRSTarget L58
def nanogravPTAResidual L61
theorem nanogravBetaHalfWidth95_pos L64
theorem nanogravRSTarget_pos L68
theorem nanograv_rs_target_inside_95_interval L75
theorem nanograv_residual_lt_half_width L82
theorem nanograv_half_width_gt_rs_target L90
theorem nanograv_dataset_attachment_status L98
structure NANOGravPTALikelihoodCert L106
def nanogravPTALikelihoodCert L121
theorem nanogravPTALikelihoodCert_inhabited L129
theorem nanograv_pta_likelihood_one_statement L134