IndisputableMonolith.Verification.EPTAPTALikelihood

   1import Mathlib
   2import IndisputableMonolith.Verification.FalsifierRegisterDatasets
   3
   4/-!
   5# EPTA DR2 PTA Likelihood Attachment
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9This module adds an EPTA DR2 scalar record to the §7 PTA stochastic-GW
  10falsifier row.
  11
  12Dataset handle:
  13
  14* EPTA DR2 / related analysis reports a stochastic-background spectral
  15  index around `γ ≈ 3.83`, with approximate asymmetric uncertainty
  16  `+0.82 / -0.72`, so the recorded interval is approximately
  17  `γ ∈ (3.11, 4.65)`.
  18
  19RS structural target:
  20
  21* `log φ ≈ 0.481`, recorded in
  22  `Verification.FalsifierRegisterDatasets.ptaAttachment.rsTargetScale`.
  23
  24Important scope:
  25
  26* EPTA's `γ` is not the same physical parameter as NANOGrav's running
  27  index `β` and is not the same as the structural RS placeholder
  28  `log φ`.
  29* The cert therefore proves two facts:
  30  1. EPTA's spectral-index interval is positive, consistent with the
  31     sign-level fact that the RS structural PTA signature is positive.
  32  2. A naive magnitude comparison would **not** place `log φ` inside
  33     the EPTA `γ` interval. This is not an RS falsification, because the
  34     dynamic RS PTA spectral-index derivation is not yet formalized.
  35
  36This is a dataset-accounting / scope-control record, not empirical
  37confirmation.
  38Zero `sorry`. Zero new RS-specific axioms.
  39-/
  40
  41namespace IndisputableMonolith
  42namespace Verification
  43namespace EPTAPTALikelihood
  44
  45open IndisputableMonolith.Verification.FalsifierRegisterDatasets
  46
  47noncomputable section
  48
  49/-! ## §1. Dataset interval and target -/
  50
  51/-- EPTA DR2 representative spectral-index central value. -/
  52def eptaGammaCentral : ℝ := 3.83
  53
  54/-- Lower endpoint using the quoted approximate `-0.72` uncertainty. -/
  55def eptaGammaLower : ℝ := 3.11
  56
  57/-- Upper endpoint using the quoted approximate `+0.82` uncertainty. -/
  58def eptaGammaUpper : ℝ := 4.65
  59
  60/-- Half-width proxy for the EPTA interval. -/
  61def eptaGammaHalfWidth : ℝ := (eptaGammaUpper - eptaGammaLower) / 2
  62
  63/-- RS structural PTA target, from the §7 dataset attachment. -/
  64def eptaRSTarget : ℝ := ptaAttachment.rsTargetScale
  65
  66/-- Naive residual between EPTA central `γ` and the structural target. -/
  67def eptaNaiveResidual : ℝ := |eptaGammaCentral - eptaRSTarget|
  68
  69theorem eptaGammaHalfWidth_pos : 0 < eptaGammaHalfWidth := by
  70  unfold eptaGammaHalfWidth eptaGammaUpper eptaGammaLower
  71  norm_num
  72
  73theorem eptaRSTarget_pos : 0 < eptaRSTarget := by
  74  unfold eptaRSTarget ptaAttachment
  75  norm_num
  76
  77/-! ## §2. Sign compatibility and honest non-match -/
  78
  79/-- EPTA's spectral-index interval is positive. -/
  80theorem epta_gamma_interval_positive :
  81    0 < eptaGammaLower ∧ eptaGammaLower < eptaGammaUpper := by
  82  unfold eptaGammaLower eptaGammaUpper
  83  norm_num
  84
  85/-- The RS structural target is below the EPTA `γ` interval. A naive
  86magnitude comparison would therefore fail. This is a scope-control
  87theorem, not a falsification theorem. -/
  88theorem epta_rs_target_below_gamma_interval :
  89    eptaRSTarget < eptaGammaLower := by
  90  unfold eptaRSTarget ptaAttachment eptaGammaLower
  91  norm_num
  92
  93/-- The naive residual is larger than the half-width. -/
  94theorem epta_naive_residual_gt_half_width :
  95    eptaGammaHalfWidth < eptaNaiveResidual := by
  96  unfold eptaNaiveResidual eptaGammaCentral eptaRSTarget ptaAttachment
  97    eptaGammaHalfWidth eptaGammaUpper eptaGammaLower
  98  norm_num
  99
 100/-- PTA dataset attachment is present, positive, and explicitly marked
 101not currently sensitive. -/
 102theorem epta_dataset_attachment_status :
 103    HasPositiveSensitivity ptaAttachment ∧
 104    HasPositiveTargetScale ptaAttachment ∧
 105    ptaAttachment.currentlySensitive = false :=
 106  ⟨pta_sensitivity_pos, pta_target_pos, rfl⟩
 107
 108/-! ## §3. Master cert -/
 109
 110structure EPTAPTALikelihoodCert where
 111  interval_positive :
 112    0 < eptaGammaLower ∧ eptaGammaLower < eptaGammaUpper
 113  target_pos : 0 < eptaRSTarget
 114  target_below_gamma_interval :
 115    eptaRSTarget < eptaGammaLower
 116  naive_residual_gt_half_width :
 117    eptaGammaHalfWidth < eptaNaiveResidual
 118  dataset_status :
 119    HasPositiveSensitivity ptaAttachment ∧
 120    HasPositiveTargetScale ptaAttachment ∧
 121    ptaAttachment.currentlySensitive = false
 122
 123def eptaPTALikelihoodCert : EPTAPTALikelihoodCert where
 124  interval_positive := epta_gamma_interval_positive
 125  target_pos := eptaRSTarget_pos
 126  target_below_gamma_interval := epta_rs_target_below_gamma_interval
 127  naive_residual_gt_half_width := epta_naive_residual_gt_half_width
 128  dataset_status := epta_dataset_attachment_status
 129
 130theorem eptaPTALikelihoodCert_inhabited :
 131    Nonempty EPTAPTALikelihoodCert :=
 132  ⟨eptaPTALikelihoodCert⟩
 133
 134/-- One-statement EPTA PTA likelihood attachment theorem. -/
 135theorem epta_pta_likelihood_one_statement :
 136    (0 < eptaGammaLower ∧ eptaGammaLower < eptaGammaUpper) ∧
 137    (0 < eptaRSTarget) ∧
 138    (eptaRSTarget < eptaGammaLower) ∧
 139    (eptaGammaHalfWidth < eptaNaiveResidual) ∧
 140    (ptaAttachment.currentlySensitive = false) ∧
 141    Nonempty EPTAPTALikelihoodCert :=
 142  ⟨epta_gamma_interval_positive,
 143   eptaRSTarget_pos,
 144   epta_rs_target_below_gamma_interval,
 145   epta_naive_residual_gt_half_width,
 146   rfl,
 147   eptaPTALikelihoodCert_inhabited⟩
 148
 149end
 150
 151end EPTAPTALikelihood
 152end Verification
 153end IndisputableMonolith
 154