IndisputableMonolith.Verification.GWTC3RingdownStatus

   1import Mathlib
   2import IndisputableMonolith.Verification.FalsifierRegisterDatasets
   3
   4/-!
   5# GWTC-3 Ringdown / Echo / QNM Status Attachment
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9This module upgrades the §7 echo/QNM falsifier rows with a concrete
  10GWTC-3 status record.
  11
  12Dataset handle:
  13
  14* LIGO/Virgo/KAGRA GWTC-3 tests of general relativity.
  15* The public abstract reports:
  16  - 15 confident signals in the analyzed O3b subset, with false alarm
  17    rates `≤ 10⁻³ yr⁻¹`;
  18  - no significant evidence for physics beyond GR;
  19  - no post-merger echoes in the analyzed events;
  20  - remnant / QNM consistency with GR;
  21  - graviton mass bound `m_g ≤ 2.42×10⁻²³ eV/c²`.
  22
  23RS structural targets:
  24
  25* Echo damping ratio `1/φ ≈ 0.618`.
  26* Rung phase delay `log φ ≈ 0.481`.
  27* Leading-log coefficient `c_RS ≈ -0.2406`.
  28
  29Important scope:
  30
  31This is **not** posterior ingestion. It is a status cert recording the
  32published GWTC-3 scalar/status facts and connecting them to the §7
  33register rows. Full likelihood-style testing of RS echo/QNM predictions
  34requires downloading and analyzing the GWTC-3 posterior release files
  35(`IGWN-GWTC3-TGR-v1-rin.zip`, etc.).
  36
  37Zero `sorry`. Zero new RS-specific axioms.
  38-/
  39
  40namespace IndisputableMonolith
  41namespace Verification
  42namespace GWTC3RingdownStatus
  43
  44open IndisputableMonolith.Verification.FalsifierRegisterDatasets
  45
  46noncomputable section
  47
  48/-! ## §1. Published scalar/status fields -/
  49
  50/-- Number of confident signals analyzed in the relevant GWTC-3 GR-tests subset. -/
  51def gwtc3AnalyzedEventCount : ℕ := 15
  52
  53/-- False alarm rate threshold for that subset, in yr⁻¹. -/
  54def gwtc3FalseAlarmRateThreshold : ℝ := 1e-3
  55
  56/-- Published GWTC-3 graviton mass bound in eV/c². -/
  57def gwtc3GravitonMassBound : ℝ := 2.42e-23
  58
  59/-- Published status: no post-merger echoes in the analyzed events. -/
  60def gwtc3NoPostMergerEchoesReported : Bool := true
  61
  62/-- Published status: no significant support for physics beyond GR. -/
  63def gwtc3NoSignificantGRDeviationReported : Bool := true
  64
  65/-- Published status: remnant/QNM consistency with GR. -/
  66def gwtc3QNMConsistentWithGR : Bool := true
  67
  68theorem gwtc3AnalyzedEventCount_pos : 0 < gwtc3AnalyzedEventCount := by
  69  unfold gwtc3AnalyzedEventCount
  70  decide
  71
  72theorem gwtc3FalseAlarmRateThreshold_pos :
  73    0 < gwtc3FalseAlarmRateThreshold := by
  74  unfold gwtc3FalseAlarmRateThreshold
  75  norm_num
  76
  77theorem gwtc3GravitonMassBound_pos : 0 < gwtc3GravitonMassBound := by
  78  unfold gwtc3GravitonMassBound
  79  norm_num
  80
  81/-! ## §2. Dataset-row connections -/
  82
  83/-- Echo row has positive sensitivity and target scale. -/
  84theorem gwtc3_echo_dataset_positive :
  85    HasPositiveSensitivity echoAttachment ∧ HasPositiveTargetScale echoAttachment :=
  86  ⟨echo_sensitivity_pos, echo_target_pos⟩
  87
  88/-- QNM row has positive sensitivity and target scale. -/
  89theorem gwtc3_qnm_dataset_positive :
  90    HasPositiveSensitivity qnmAttachment ∧ HasPositiveTargetScale qnmAttachment :=
  91  ⟨qnm_sensitivity_pos, qnm_target_pos⟩
  92
  93/-- Published qualitative statuses are all recorded as true. -/
  94theorem gwtc3_status_flags :
  95    gwtc3NoPostMergerEchoesReported = true ∧
  96    gwtc3NoSignificantGRDeviationReported = true ∧
  97    gwtc3QNMConsistentWithGR = true :=
  98  ⟨rfl, rfl, rfl⟩
  99
 100/-! ## §3. Master cert -/
 101
 102structure GWTC3RingdownStatusCert where
 103  event_count_pos : 0 < gwtc3AnalyzedEventCount
 104  far_threshold_pos : 0 < gwtc3FalseAlarmRateThreshold
 105  graviton_mass_bound_pos : 0 < gwtc3GravitonMassBound
 106  echo_dataset_positive :
 107    HasPositiveSensitivity echoAttachment ∧ HasPositiveTargetScale echoAttachment
 108  qnm_dataset_positive :
 109    HasPositiveSensitivity qnmAttachment ∧ HasPositiveTargetScale qnmAttachment
 110  status_flags :
 111    gwtc3NoPostMergerEchoesReported = true ∧
 112    gwtc3NoSignificantGRDeviationReported = true ∧
 113    gwtc3QNMConsistentWithGR = true
 114
 115def gwtc3RingdownStatusCert : GWTC3RingdownStatusCert where
 116  event_count_pos := gwtc3AnalyzedEventCount_pos
 117  far_threshold_pos := gwtc3FalseAlarmRateThreshold_pos
 118  graviton_mass_bound_pos := gwtc3GravitonMassBound_pos
 119  echo_dataset_positive := gwtc3_echo_dataset_positive
 120  qnm_dataset_positive := gwtc3_qnm_dataset_positive
 121  status_flags := gwtc3_status_flags
 122
 123theorem gwtc3RingdownStatusCert_inhabited :
 124    Nonempty GWTC3RingdownStatusCert :=
 125  ⟨gwtc3RingdownStatusCert⟩
 126
 127/-- One-statement GWTC-3 status attachment theorem. -/
 128theorem gwtc3_ringdown_status_one_statement :
 129    (0 < gwtc3AnalyzedEventCount) ∧
 130    (0 < gwtc3FalseAlarmRateThreshold) ∧
 131    (0 < gwtc3GravitonMassBound) ∧
 132    (gwtc3NoPostMergerEchoesReported = true) ∧
 133    (gwtc3NoSignificantGRDeviationReported = true) ∧
 134    (gwtc3QNMConsistentWithGR = true) ∧
 135    Nonempty GWTC3RingdownStatusCert :=
 136  ⟨gwtc3AnalyzedEventCount_pos,
 137   gwtc3FalseAlarmRateThreshold_pos,
 138   gwtc3GravitonMassBound_pos,
 139   rfl, rfl, rfl,
 140   gwtc3RingdownStatusCert_inhabited⟩
 141
 142end
 143
 144end GWTC3RingdownStatus
 145end Verification
 146end IndisputableMonolith
 147