IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy
   3import IndisputableMonolith.Verification.GWTC3RingdownOneMemberDampingStatistic
   4
   5/-!
   6# GWTC-3 Ringdown DS_1mode_10M Family Damping Statistic
   7
   8## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   9
  10This module records the first controlled-family scaling of the Session
  11123 one-member QNM damping statistic.
  12
  13Family:
  14
  15* model `DS_1mode_10M`
  16* 22 HDF5 files
  17* 22 events
  18* 643,624 pooled posterior samples
  19
  20Observable:
  21
  22* `damping_per_cycle = exp(-1 / (f_t_0 * tau_t_0))`
  23
  24RS target:
  25
  26* `1/φ ≈ 0.618033988750`
  27
  28Result:
  29
  30* pooled mean `0.581257730777`
  31* pooled std `0.264599094550`
  32* pooled median `0.569663372044`
  33* pooled q05/q95 `0.118026458809 / 0.958639185642`
  34* pooled q16/q84 `0.292577350498 / 0.898893346068`
  35* target inside pooled 90% and 68% intervals
  36* 13 of 22 member-level intervals contain the target in the central 68%
  37
  38This is controlled-family only. It does not mix Kerr, MMRDNP, and
  39waveform-model semantics; it is not a full archive likelihood.
  40
  41Zero `sorry`. Zero new RS-specific axioms.
  42-/
  43
  44namespace IndisputableMonolith
  45namespace Verification
  46namespace GWTC3RingdownDS1Mode10MDampingFamily
  47
  48open IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy
  49open IndisputableMonolith.Verification.GWTC3RingdownOneMemberDampingStatistic
  50
  51/-! ## §1. Family constants -/
  52
  53def dsFamilyModelName : String := "DS_1mode_10M"
  54def dsFamilyMemberCount : Nat := 22
  55def dsFamilyEventCount : Nat := 22
  56def dsFamilyTotalSampleCount : Nat := 643624
  57def dsRSDampingTarget : ℝ := 0.618033988750
  58def dsPooledMean : ℝ := 0.581257730777
  59def dsPooledStd : ℝ := 0.264599094550
  60def dsPooledMedian : ℝ := 0.569663372044
  61def dsPooledQ05 : ℝ := 0.118026458809
  62def dsPooledQ16 : ℝ := 0.292577350498
  63def dsPooledQ84 : ℝ := 0.898893346068
  64def dsPooledQ95 : ℝ := 0.958639185642
  65def dsPooledZFromMean : ℝ := 0.138989
  66def dsPooledFractionBelowTarget : ℝ := 0.560888
  67def dsMembersInside68Count : Nat := 13
  68
  69/-! ## §2. Count and interval facts -/
  70
  71theorem ds_family_member_count_matches_taxonomy :
  72    dsFamilyMemberCount = taxonomyDampedSinusoidCount := rfl
  73
  74theorem ds_family_event_count_pos : 0 < dsFamilyEventCount := by
  75  unfold dsFamilyEventCount
  76  decide
  77
  78theorem ds_family_sample_count_pos : 0 < dsFamilyTotalSampleCount := by
  79  unfold dsFamilyTotalSampleCount
  80  decide
  81
  82theorem ds_target_inside_pooled_90 :
  83    dsPooledQ05 < dsRSDampingTarget ∧ dsRSDampingTarget < dsPooledQ95 := by
  84  unfold dsPooledQ05 dsRSDampingTarget dsPooledQ95
  85  norm_num
  86
  87theorem ds_target_inside_pooled_68 :
  88    dsPooledQ16 < dsRSDampingTarget ∧ dsRSDampingTarget < dsPooledQ84 := by
  89  unfold dsPooledQ16 dsRSDampingTarget dsPooledQ84
  90  norm_num
  91
  92theorem ds_z_from_mean_lt_one :
  93    dsPooledZFromMean < 1 := by
  94  unfold dsPooledZFromMean
  95  norm_num
  96
  97theorem ds_fraction_below_target_valid :
  98    0 < dsPooledFractionBelowTarget ∧ dsPooledFractionBelowTarget < 1 := by
  99  unfold dsPooledFractionBelowTarget
 100  norm_num
 101
 102theorem ds_members_inside68_nonzero :
 103    0 < dsMembersInside68Count ∧ dsMembersInside68Count < dsFamilyMemberCount := by
 104  unfold dsMembersInside68Count dsFamilyMemberCount
 105  decide
 106
 107/-! ## §3. Master cert -/
 108
 109structure GWTC3RingdownDS1Mode10MDampingFamilyCert where
 110  member_count_matches_taxonomy :
 111    dsFamilyMemberCount = taxonomyDampedSinusoidCount
 112  event_count_pos : 0 < dsFamilyEventCount
 113  sample_count_pos : 0 < dsFamilyTotalSampleCount
 114  target_inside_pooled_90 :
 115    dsPooledQ05 < dsRSDampingTarget ∧ dsRSDampingTarget < dsPooledQ95
 116  target_inside_pooled_68 :
 117    dsPooledQ16 < dsRSDampingTarget ∧ dsRSDampingTarget < dsPooledQ84
 118  z_lt_one : dsPooledZFromMean < 1
 119  fraction_valid :
 120    0 < dsPooledFractionBelowTarget ∧ dsPooledFractionBelowTarget < 1
 121  member_inside_count_nonzero :
 122    0 < dsMembersInside68Count ∧ dsMembersInside68Count < dsFamilyMemberCount
 123  taxonomy_available : Nonempty GWTC3RingdownFilenameTaxonomyCert
 124  one_member_damping_available : Nonempty GWTC3RingdownOneMemberDampingStatisticCert
 125
 126def gwtc3RingdownDS1Mode10MDampingFamilyCert :
 127    GWTC3RingdownDS1Mode10MDampingFamilyCert where
 128  member_count_matches_taxonomy := ds_family_member_count_matches_taxonomy
 129  event_count_pos := ds_family_event_count_pos
 130  sample_count_pos := ds_family_sample_count_pos
 131  target_inside_pooled_90 := ds_target_inside_pooled_90
 132  target_inside_pooled_68 := ds_target_inside_pooled_68
 133  z_lt_one := ds_z_from_mean_lt_one
 134  fraction_valid := ds_fraction_below_target_valid
 135  member_inside_count_nonzero := ds_members_inside68_nonzero
 136  taxonomy_available := gwtc3RingdownFilenameTaxonomyCert_inhabited
 137  one_member_damping_available := gwtc3RingdownOneMemberDampingStatisticCert_inhabited
 138
 139theorem gwtc3RingdownDS1Mode10MDampingFamilyCert_inhabited :
 140    Nonempty GWTC3RingdownDS1Mode10MDampingFamilyCert :=
 141  ⟨gwtc3RingdownDS1Mode10MDampingFamilyCert⟩
 142
 143/-- One-statement controlled-family damping theorem. -/
 144theorem gwtc3_ringdown_ds1mode10m_damping_family_one_statement :
 145    (dsFamilyMemberCount = 22) ∧
 146    (dsFamilyEventCount = 22) ∧
 147    (dsFamilyTotalSampleCount = 643624) ∧
 148    (dsPooledQ05 < dsRSDampingTarget ∧ dsRSDampingTarget < dsPooledQ95) ∧
 149    (dsPooledQ16 < dsRSDampingTarget ∧ dsRSDampingTarget < dsPooledQ84) ∧
 150    (dsPooledZFromMean < 1) ∧
 151    Nonempty GWTC3RingdownDS1Mode10MDampingFamilyCert :=
 152  ⟨rfl, rfl, rfl,
 153   ds_target_inside_pooled_90,
 154   ds_target_inside_pooled_68,
 155   ds_z_from_mean_lt_one,
 156   gwtc3RingdownDS1Mode10MDampingFamilyCert_inhabited⟩
 157
 158end GWTC3RingdownDS1Mode10MDampingFamily
 159end Verification
 160end IndisputableMonolith
 161