IndisputableMonolith.Verification.GWTC3RingdownOneMemberDampingStatistic

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary
   3
   4/-!
   5# GWTC-3 Ringdown One-Member QNM Damping Statistic
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9This module records the first physically mapped one-member GWTC-3
  10ringdown statistic:
  11
  12`f_t_0` and `tau_t_0` are mapped to the per-cycle QNM damping ratio
  13
  14`damping_per_cycle = exp(-1 / (f_t_0 * tau_t_0))`.
  15
  16The RS structural echo damping target is `1/φ ≈ 0.618033988750`.
  17
  18For the range-read sample member
  19`rin/rin_S190727h_pyring_DS_1mode_10M.h5`, the target lies inside the
  20central 68% and 90% intervals of the derived damping statistic.
  21
  22This is one-member damping comparison only. It is not archive-wide and
  23does not establish that single-mode QNM damping per cycle is identical
  24to the final RS echo-train damping observable.
  25
  26Zero `sorry`. Zero new RS-specific axioms.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Verification
  31namespace GWTC3RingdownOneMemberDampingStatistic
  32
  33open IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary
  34
  35/-! ## §1. Statistic constants -/
  36
  37def rsDampingTarget : ℝ := 0.618033988750
  38def dampingMean : ℝ := 0.764591716607
  39def dampingStd : ℝ := 0.220115833630
  40def dampingMedian : ℝ := 0.845646710036
  41def dampingQ05 : ℝ := 0.279244551922
  42def dampingQ16 : ℝ := 0.552717258546
  43def dampingQ84 : ℝ := 0.950497542361
  44def dampingQ95 : ℝ := 0.969863091765
  45def dampingResidualFromMean : ℝ := 0.146557727857
  46def dampingZFromMean : ℝ := 0.665820924556
  47def dampingFractionBelowTarget : ℝ := 0.208416038110
  48def ftauMean : ℝ := 9.950564161770
  49def rsFtauTarget : ℝ := 2.078086921235
  50
  51/-! ## §2. Interval and sign facts -/
  52
  53theorem damping_target_inside_90_interval :
  54    dampingQ05 < rsDampingTarget ∧ rsDampingTarget < dampingQ95 := by
  55  unfold dampingQ05 rsDampingTarget dampingQ95
  56  norm_num
  57
  58theorem damping_target_inside_68_interval :
  59    dampingQ16 < rsDampingTarget ∧ rsDampingTarget < dampingQ84 := by
  60  unfold dampingQ16 rsDampingTarget dampingQ84
  61  norm_num
  62
  63theorem damping_z_from_mean_lt_one :
  64    dampingZFromMean < 1 := by
  65  unfold dampingZFromMean
  66  norm_num
  67
  68theorem damping_fraction_below_target_between_zero_and_one :
  69    0 < dampingFractionBelowTarget ∧ dampingFractionBelowTarget < 1 := by
  70  unfold dampingFractionBelowTarget
  71  norm_num
  72
  73theorem ftau_mean_gt_rs_target :
  74    rsFtauTarget < ftauMean := by
  75  unfold rsFtauTarget ftauMean
  76  norm_num
  77
  78theorem sample_summary_available :
  79    Nonempty GWTC3RingdownHDF5SampleSummaryCert :=
  80  gwtc3RingdownHDF5SampleSummaryCert_inhabited
  81
  82/-! ## §3. Master cert -/
  83
  84structure GWTC3RingdownOneMemberDampingStatisticCert where
  85  target_inside_90 :
  86    dampingQ05 < rsDampingTarget ∧ rsDampingTarget < dampingQ95
  87  target_inside_68 :
  88    dampingQ16 < rsDampingTarget ∧ rsDampingTarget < dampingQ84
  89  z_lt_one : dampingZFromMean < 1
  90  fraction_valid :
  91    0 < dampingFractionBelowTarget ∧ dampingFractionBelowTarget < 1
  92  ftau_gt_target : rsFtauTarget < ftauMean
  93  sample_summary_available : Nonempty GWTC3RingdownHDF5SampleSummaryCert
  94
  95def gwtc3RingdownOneMemberDampingStatisticCert :
  96    GWTC3RingdownOneMemberDampingStatisticCert where
  97  target_inside_90 := damping_target_inside_90_interval
  98  target_inside_68 := damping_target_inside_68_interval
  99  z_lt_one := damping_z_from_mean_lt_one
 100  fraction_valid := damping_fraction_below_target_between_zero_and_one
 101  ftau_gt_target := ftau_mean_gt_rs_target
 102  sample_summary_available := sample_summary_available
 103
 104theorem gwtc3RingdownOneMemberDampingStatisticCert_inhabited :
 105    Nonempty GWTC3RingdownOneMemberDampingStatisticCert :=
 106  ⟨gwtc3RingdownOneMemberDampingStatisticCert⟩
 107
 108/-- One-statement theorem for the one-member damping statistic. -/
 109theorem gwtc3_ringdown_one_member_damping_statistic_one_statement :
 110    (dampingQ05 < rsDampingTarget ∧ rsDampingTarget < dampingQ95) ∧
 111    (dampingQ16 < rsDampingTarget ∧ rsDampingTarget < dampingQ84) ∧
 112    (dampingZFromMean < 1) ∧
 113    Nonempty GWTC3RingdownOneMemberDampingStatisticCert :=
 114  ⟨damping_target_inside_90_interval,
 115   damping_target_inside_68_interval,
 116   damping_z_from_mean_lt_one,
 117   gwtc3RingdownOneMemberDampingStatisticCert_inhabited⟩
 118
 119end GWTC3RingdownOneMemberDampingStatistic
 120end Verification
 121end IndisputableMonolith
 122