Verification Nanograv Ptalikelihood

A consistency certificate

Recognition Science (a framework that derives physical structure from the forced cost of recognition events) maintains a falsifier register: a list of dataset rows, each pairing a structural prediction with a measured interval. The verification nanograv ptalikelihood module attaches a dataset-specific certificate to the row for the NANOGrav 15-year pulsar timing array analysis. Pulsar timing arrays are networks of millisecond pulsars whose radio pulse arrival times are monitored for correlated deviations, a signature of a stochastic gravitational wave background.

The certificate concerns the running spectral index β, a parameter describing how the gravitational wave background's spectral slope changes with frequency. NANOGrav's 15-year running spectral-index analysis reported a broad 95% credible interval for β, approximately from -0.80 to 2.96. The Recognition Science structural target for this dataset is log φ ≈ 0.481, a number derived from the framework's golden ratio scaling. The central theorem proves that this target lies strictly inside the reported interval, and that the residual between the target and the interval midpoint is smaller than the interval half-width.

The module is explicit about what this does not mean. A companion theorem proves the interval half-width is larger than the target itself, and the dataset row is marked not currently sensitive in the falsifier register. The certificate is a consistency and non-sensitivity test, not empirical confirmation. The framework's library of formal theorems checks these facts with zero unproved assumptions, but the honesty of the result lies in what it refuses to claim: the data are too coarse to test the prediction.

In plain language, the module says: the Recognition Science prediction does not contradict the NANOGrav measurement, but the measurement is not precise enough to confirm the prediction either. This is the framework's falsifier register working as designed, recording a structural target that survives a first coarse look at the data while flagging that the look is not yet a test. The certificate is a structural theorem, not an empirical result, and it carries no claim that the framework has been validated by the pulsar data.

/-- RS structural PTA target, from the §7 dataset attachment. -/
def nanogravRSTarget : ℝ := ptaAttachment.rsTargetScale

/-- The RS structural target lies inside the reported NANOGrav β interval. -/
theorem nanograv_rs_target_inside_95_interval :
    nanogravBetaLower95 < nanogravRSTarget ∧
      nanogravRSTarget < nanogravBetaUpper95 := by
  unfold nanogravBetaLower95 nanogravBetaUpper95 nanogravRSTarget ptaAttachment
  norm_num

/-- Residual from midpoint is smaller than the interval half-width. -/
theorem nanograv_residual_lt_half_width :
    nanogravPTAResidual < nanogravBetaHalfWidth95 := by
  unfold nanogravPTAResidual nanogravBetaMidpoint nanogravBetaHalfWidth95
    nanogravBetaLower95 nanogravBetaUpper95 nanogravRSTarget ptaAttachment
  norm_num

/-- The broad interval is not yet sensitive to the RS target scale:
the half-width is larger than the target itself. -/
theorem nanograv_half_width_gt_rs_target :
    nanogravRSTarget < nanogravBetaHalfWidth95 := by
  unfold nanogravRSTarget ptaAttachment nanogravBetaHalfWidth95
    nanogravBetaUpper95 nanogravBetaLower95
  norm_num

/-- PTA dataset attachment is present, positive, and explicitly marked
not currently sensitive. -/
theorem nanograv_dataset_attachment_status :
    HasPositiveSensitivity ptaAttachment ∧
    HasPositiveTargetScale ptaAttachment ∧
    ptaAttachment.currentlySensitive = false :=
  ⟨pta_sensitivity_pos, pta_target_pos, rfl⟩

/-- One-statement NANOGrav PTA likelihood attachment theorem. -/
theorem nanograv_pta_likelihood_one_statement :
    (nanogravBetaLower95 < nanogravRSTarget ∧
      nanogravRSTarget < nanogravBetaUpper95) ∧
    (nanogravPTAResidual < nanogravBetaHalfWidth95) ∧
    (nanogravRSTarget < nanogravBetaHalfWidth95) ∧
    (ptaAttachment.currentlySensitive = false) ∧
    Nonempty NANOGravPTALikelihoodCert :=
  ⟨nanograv_rs_target_inside_95_interval,
   nanograv_residual_lt_half_width,
   nanograv_half_width_gt_rs_target,
   rfl,
   nanogravPTALikelihoodCert_inhabited⟩

What this page does not claim

The NANOGrav data confirm the Recognition Science prediction. The module derives the NANOGrav interval from first principles. The certificate establishes that the target is the best explanation of the data.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/NANOGravPTALikelihood.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: