IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy
   3import IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily
   4
   5/-!
   6# GWTC-3 Ringdown Kerr_220_0M 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 Kerr-family scaling of the QNM
  11damping statistic.
  12
  13Family:
  14
  15* model `Kerr_220_0M`
  16* 22 HDF5 files
  17* 22 events
  18* 647,220 pooled posterior samples
  19
  20Observable:
  21
  22For Kerr files the posterior table has `af` rather than explicit
  23`f_t_0` and `tau_t_0`. The companion script uses the standard Berti-style
  24Kerr-220 quality-factor fit
  25
  26`Q_220(a) = 0.7000 + 1.4187 (1-a)^(-0.4990)`
  27
  28and maps it to
  29
  30`damping_per_cycle = exp(-π / Q_220)`.
  31
  32RS target:
  33
  34* `1/φ ≈ 0.618033988750`
  35
  36Result:
  37
  38* pooled mean `0.438208510863`
  39* pooled std `0.122250226107`
  40* pooled median `0.433285700166`
  41* pooled q05/q95 `0.249303771620 / 0.643869947920`
  42* pooled q16/q84 `0.299869164713 / 0.575770415071`
  43* target inside pooled 90% but not inside pooled 68%
  44* 3 of 22 member-level central 68% intervals contain the target
  45
  46This is controlled-family only. It is not a full archive likelihood.
  47Zero `sorry`. Zero new RS-specific axioms.
  48-/
  49
  50namespace IndisputableMonolith
  51namespace Verification
  52namespace GWTC3RingdownKerr2200MDampingFamily
  53
  54open IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy
  55open IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily
  56
  57/-! ## §1. Family constants -/
  58
  59def kerr2200ModelName : String := "Kerr_220_0M"
  60def kerr2200MemberCount : Nat := 22
  61def kerr2200EventCount : Nat := 22
  62def kerr2200TotalSampleCount : Nat := 647220
  63def kerr2200RSDampingTarget : ℝ := 0.618033988750
  64def kerr2200PooledMean : ℝ := 0.438208510863
  65def kerr2200PooledStd : ℝ := 0.122250226107
  66def kerr2200PooledMedian : ℝ := 0.433285700166
  67def kerr2200PooledQ05 : ℝ := 0.249303771620
  68def kerr2200PooledQ16 : ℝ := 0.299869164713
  69def kerr2200PooledQ84 : ℝ := 0.575770415071
  70def kerr2200PooledQ95 : ℝ := 0.643869947920
  71def kerr2200PooledZFromMean : ℝ := 1.470962
  72def kerr2200PooledFractionBelowTarget : ℝ := 0.914513
  73def kerr2200MembersInside68Count : Nat := 3
  74
  75/-! ## §2. Count and interval facts -/
  76
  77theorem kerr2200_member_count_pos : 0 < kerr2200MemberCount := by
  78  unfold kerr2200MemberCount
  79  decide
  80
  81theorem kerr2200_event_count_pos : 0 < kerr2200EventCount := by
  82  unfold kerr2200EventCount
  83  decide
  84
  85theorem kerr2200_sample_count_pos : 0 < kerr2200TotalSampleCount := by
  86  unfold kerr2200TotalSampleCount
  87  decide
  88
  89theorem kerr2200_target_inside_pooled_90 :
  90    kerr2200PooledQ05 < kerr2200RSDampingTarget ∧
  91      kerr2200RSDampingTarget < kerr2200PooledQ95 := by
  92  unfold kerr2200PooledQ05 kerr2200RSDampingTarget kerr2200PooledQ95
  93  norm_num
  94
  95theorem kerr2200_target_not_inside_pooled_68 :
  96    kerr2200PooledQ84 < kerr2200RSDampingTarget := by
  97  unfold kerr2200PooledQ84 kerr2200RSDampingTarget
  98  norm_num
  99
 100theorem kerr2200_z_from_mean_gt_one :
 101    1 < kerr2200PooledZFromMean := by
 102  unfold kerr2200PooledZFromMean
 103  norm_num
 104
 105theorem kerr2200_fraction_below_target_valid :
 106    0 < kerr2200PooledFractionBelowTarget ∧ kerr2200PooledFractionBelowTarget < 1 := by
 107  unfold kerr2200PooledFractionBelowTarget
 108  norm_num
 109
 110theorem kerr2200_members_inside68_nonzero :
 111    0 < kerr2200MembersInside68Count ∧ kerr2200MembersInside68Count < kerr2200MemberCount := by
 112  unfold kerr2200MembersInside68Count kerr2200MemberCount
 113  decide
 114
 115theorem ds_vs_kerr_mean_order :
 116    kerr2200PooledMean < dsPooledMean := by
 117  unfold kerr2200PooledMean dsPooledMean
 118  norm_num
 119
 120/-! ## §3. Master cert -/
 121
 122structure GWTC3RingdownKerr2200MDampingFamilyCert where
 123  member_count_pos : 0 < kerr2200MemberCount
 124  event_count_pos : 0 < kerr2200EventCount
 125  sample_count_pos : 0 < kerr2200TotalSampleCount
 126  target_inside_pooled_90 :
 127    kerr2200PooledQ05 < kerr2200RSDampingTarget ∧
 128      kerr2200RSDampingTarget < kerr2200PooledQ95
 129  target_not_inside_pooled_68 :
 130    kerr2200PooledQ84 < kerr2200RSDampingTarget
 131  z_gt_one : 1 < kerr2200PooledZFromMean
 132  fraction_valid :
 133    0 < kerr2200PooledFractionBelowTarget ∧ kerr2200PooledFractionBelowTarget < 1
 134  member_inside_count_nonzero :
 135    0 < kerr2200MembersInside68Count ∧ kerr2200MembersInside68Count < kerr2200MemberCount
 136  ds_mean_greater :
 137    kerr2200PooledMean < dsPooledMean
 138  taxonomy_available : Nonempty GWTC3RingdownFilenameTaxonomyCert
 139  ds_family_available : Nonempty GWTC3RingdownDS1Mode10MDampingFamilyCert
 140
 141def gwtc3RingdownKerr2200MDampingFamilyCert :
 142    GWTC3RingdownKerr2200MDampingFamilyCert where
 143  member_count_pos := kerr2200_member_count_pos
 144  event_count_pos := kerr2200_event_count_pos
 145  sample_count_pos := kerr2200_sample_count_pos
 146  target_inside_pooled_90 := kerr2200_target_inside_pooled_90
 147  target_not_inside_pooled_68 := kerr2200_target_not_inside_pooled_68
 148  z_gt_one := kerr2200_z_from_mean_gt_one
 149  fraction_valid := kerr2200_fraction_below_target_valid
 150  member_inside_count_nonzero := kerr2200_members_inside68_nonzero
 151  ds_mean_greater := ds_vs_kerr_mean_order
 152  taxonomy_available := gwtc3RingdownFilenameTaxonomyCert_inhabited
 153  ds_family_available := gwtc3RingdownDS1Mode10MDampingFamilyCert_inhabited
 154
 155theorem gwtc3RingdownKerr2200MDampingFamilyCert_inhabited :
 156    Nonempty GWTC3RingdownKerr2200MDampingFamilyCert :=
 157  ⟨gwtc3RingdownKerr2200MDampingFamilyCert⟩
 158
 159/-- One-statement Kerr-family damping theorem. -/
 160theorem gwtc3_ringdown_kerr2200m_damping_family_one_statement :
 161    (kerr2200MemberCount = 22) ∧
 162    (kerr2200EventCount = 22) ∧
 163    (kerr2200TotalSampleCount = 647220) ∧
 164    (kerr2200PooledQ05 < kerr2200RSDampingTarget ∧
 165      kerr2200RSDampingTarget < kerr2200PooledQ95) ∧
 166    (kerr2200PooledQ84 < kerr2200RSDampingTarget) ∧
 167    (kerr2200PooledMean < dsPooledMean) ∧
 168    Nonempty GWTC3RingdownKerr2200MDampingFamilyCert :=
 169  ⟨rfl, rfl, rfl,
 170   kerr2200_target_inside_pooled_90,
 171   kerr2200_target_not_inside_pooled_68,
 172   ds_vs_kerr_mean_order,
 173   gwtc3RingdownKerr2200MDampingFamilyCert_inhabited⟩
 174
 175end GWTC3RingdownKerr2200MDampingFamily
 176end Verification
 177end IndisputableMonolith
 178