IndisputableMonolith.Verification.NANOGravPTALikelihood

   1import Mathlib
   2import IndisputableMonolith.Verification.FalsifierRegisterDatasets
   3
   4/-!
   5# NANOGrav PTA Likelihood Attachment
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9This module upgrades the §7 PTA stochastic-GW falsifier row with a
  10dataset-specific likelihood-style certificate.
  11
  12Dataset handle:
  13
  14* NANOGrav 15-year running spectral-index analysis reports a broad
  15  95% credible interval for the running parameter β consistent with
  16  zero, approximately `β ∈ [-0.80, 2.96]`.
  17
  18RS structural target:
  19
  20* `log φ ≈ 0.481`, recorded in
  21  `Verification.FalsifierRegisterDatasets.ptaAttachment.rsTargetScale`.
  22
  23The certificate proves two honest facts:
  24
  251. The RS structural target lies inside the reported broad NANOGrav
  26   95% interval.
  272. The interval is not yet a confirmation of RS: the target is much
  28   smaller than the interval width, and the dataset row remains marked
  29   not currently sensitive in the falsifier-register attachment.
  30
  31This is a consistency / non-sensitivity test, not empirical confirmation.
  32Zero `sorry`. Zero new RS-specific axioms.
  33-/
  34
  35namespace IndisputableMonolith
  36namespace Verification
  37namespace NANOGravPTALikelihood
  38
  39open IndisputableMonolith.Verification.FalsifierRegisterDatasets
  40
  41noncomputable section
  42
  43/-! ## §1. Dataset interval and target -/
  44
  45/-- Lower endpoint of the reported broad NANOGrav 95% β interval. -/
  46def nanogravBetaLower95 : ℝ := -0.80
  47
  48/-- Upper endpoint of the reported broad NANOGrav 95% β interval. -/
  49def nanogravBetaUpper95 : ℝ := 2.96
  50
  51/-- Midpoint of the interval, used only for a likelihood-style residual. -/
  52def nanogravBetaMidpoint : ℝ := (nanogravBetaLower95 + nanogravBetaUpper95) / 2
  53
  54/-- Half-width of the 95% interval, used as a conservative sensitivity scale. -/
  55def nanogravBetaHalfWidth95 : ℝ := (nanogravBetaUpper95 - nanogravBetaLower95) / 2
  56
  57/-- RS structural PTA target, from the §7 dataset attachment. -/
  58def nanogravRSTarget : ℝ := ptaAttachment.rsTargetScale
  59
  60/-- Residual between interval midpoint and RS target. -/
  61def nanogravPTAResidual : ℝ :=
  62  |nanogravBetaMidpoint - nanogravRSTarget|
  63
  64theorem nanogravBetaHalfWidth95_pos : 0 < nanogravBetaHalfWidth95 := by
  65  unfold nanogravBetaHalfWidth95 nanogravBetaUpper95 nanogravBetaLower95
  66  norm_num
  67
  68theorem nanogravRSTarget_pos : 0 < nanogravRSTarget := by
  69  unfold nanogravRSTarget ptaAttachment
  70  norm_num
  71
  72/-! ## §2. Interval inclusion and non-sensitivity -/
  73
  74/-- The RS structural target lies inside the reported NANOGrav β interval. -/
  75theorem nanograv_rs_target_inside_95_interval :
  76    nanogravBetaLower95 < nanogravRSTarget ∧
  77      nanogravRSTarget < nanogravBetaUpper95 := by
  78  unfold nanogravBetaLower95 nanogravBetaUpper95 nanogravRSTarget ptaAttachment
  79  norm_num
  80
  81/-- Residual from midpoint is smaller than the interval half-width. -/
  82theorem nanograv_residual_lt_half_width :
  83    nanogravPTAResidual < nanogravBetaHalfWidth95 := by
  84  unfold nanogravPTAResidual nanogravBetaMidpoint nanogravBetaHalfWidth95
  85    nanogravBetaLower95 nanogravBetaUpper95 nanogravRSTarget ptaAttachment
  86  norm_num
  87
  88/-- The broad interval is not yet sensitive to the RS target scale:
  89the half-width is larger than the target itself. -/
  90theorem nanograv_half_width_gt_rs_target :
  91    nanogravRSTarget < nanogravBetaHalfWidth95 := by
  92  unfold nanogravRSTarget ptaAttachment nanogravBetaHalfWidth95
  93    nanogravBetaUpper95 nanogravBetaLower95
  94  norm_num
  95
  96/-- PTA dataset attachment is present, positive, and explicitly marked
  97not currently sensitive. -/
  98theorem nanograv_dataset_attachment_status :
  99    HasPositiveSensitivity ptaAttachment ∧
 100    HasPositiveTargetScale ptaAttachment ∧
 101    ptaAttachment.currentlySensitive = false :=
 102  ⟨pta_sensitivity_pos, pta_target_pos, rfl⟩
 103
 104/-! ## §3. Master cert -/
 105
 106structure NANOGravPTALikelihoodCert where
 107  half_width_pos : 0 < nanogravBetaHalfWidth95
 108  target_pos : 0 < nanogravRSTarget
 109  target_inside_interval :
 110    nanogravBetaLower95 < nanogravRSTarget ∧
 111      nanogravRSTarget < nanogravBetaUpper95
 112  residual_lt_half_width :
 113    nanogravPTAResidual < nanogravBetaHalfWidth95
 114  not_currently_sensitive :
 115    nanogravRSTarget < nanogravBetaHalfWidth95
 116  dataset_status :
 117    HasPositiveSensitivity ptaAttachment ∧
 118    HasPositiveTargetScale ptaAttachment ∧
 119    ptaAttachment.currentlySensitive = false
 120
 121def nanogravPTALikelihoodCert : NANOGravPTALikelihoodCert where
 122  half_width_pos := nanogravBetaHalfWidth95_pos
 123  target_pos := nanogravRSTarget_pos
 124  target_inside_interval := nanograv_rs_target_inside_95_interval
 125  residual_lt_half_width := nanograv_residual_lt_half_width
 126  not_currently_sensitive := nanograv_half_width_gt_rs_target
 127  dataset_status := nanograv_dataset_attachment_status
 128
 129theorem nanogravPTALikelihoodCert_inhabited :
 130    Nonempty NANOGravPTALikelihoodCert :=
 131  ⟨nanogravPTALikelihoodCert⟩
 132
 133/-- One-statement NANOGrav PTA likelihood attachment theorem. -/
 134theorem nanograv_pta_likelihood_one_statement :
 135    (nanogravBetaLower95 < nanogravRSTarget ∧
 136      nanogravRSTarget < nanogravBetaUpper95) ∧
 137    (nanogravPTAResidual < nanogravBetaHalfWidth95) ∧
 138    (nanogravRSTarget < nanogravBetaHalfWidth95) ∧
 139    (ptaAttachment.currentlySensitive = false) ∧
 140    Nonempty NANOGravPTALikelihoodCert :=
 141  ⟨nanograv_rs_target_inside_95_interval,
 142   nanograv_residual_lt_half_width,
 143   nanograv_half_width_gt_rs_target,
 144   rfl,
 145   nanogravPTALikelihoodCert_inhabited⟩
 146
 147end
 148
 149end NANOGravPTALikelihood
 150end Verification
 151end IndisputableMonolith
 152