IndisputableMonolith.Verification.GWTC3RingdownKerr22010MDampingFamily

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily
   3
   4/-!
   5# GWTC-3 Ringdown Kerr_220_10M Family Damping Statistic
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9This module records the second controlled Kerr-family damping statistic.
  10It keeps the same Kerr 220 QNM mode as Session 128 but changes the
  11ringdown start-time window to `10M`.
  12
  13Family:
  14
  15* model `Kerr_220_10M`
  16* 22 HDF5 files
  17* 22 events
  18* 664,154 pooled posterior samples
  19
  20Result:
  21
  22* pooled mean `0.348730205961`
  23* pooled std `0.103850136706`
  24* pooled median `0.320171053042`
  25* pooled q05/q95 `0.233283419046 / 0.546003135309`
  26* pooled q16/q84 `0.248744219541 / 0.459021150603`
  27* target `1/φ` outside pooled 90% and 68% intervals
  28* 0 of 22 member-level central 68% intervals contain the target
  29
  30This is controlled-family only. It is not a full archive likelihood.
  31Zero `sorry`. Zero new RS-specific axioms.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Verification
  36namespace GWTC3RingdownKerr22010MDampingFamily
  37
  38open IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily
  39
  40/-! ## §1. Family constants -/
  41
  42def kerr22010ModelName : String := "Kerr_220_10M"
  43def kerr22010MemberCount : Nat := 22
  44def kerr22010EventCount : Nat := 22
  45def kerr22010TotalSampleCount : Nat := 664154
  46def kerr22010RSDampingTarget : ℝ := 0.618033988750
  47def kerr22010PooledMean : ℝ := 0.348730205961
  48def kerr22010PooledStd : ℝ := 0.103850136706
  49def kerr22010PooledMedian : ℝ := 0.320171053042
  50def kerr22010PooledQ05 : ℝ := 0.233283419046
  51def kerr22010PooledQ16 : ℝ := 0.248744219541
  52def kerr22010PooledQ84 : ℝ := 0.459021150603
  53def kerr22010PooledQ95 : ℝ := 0.546003135309
  54def kerr22010PooledZFromMean : ℝ := 2.593196
  55def kerr22010PooledFractionBelowTarget : ℝ := 0.981447
  56def kerr22010MembersInside68Count : Nat := 0
  57
  58/-! ## §2. Count and interval facts -/
  59
  60theorem kerr22010_member_count_pos : 0 < kerr22010MemberCount := by
  61  unfold kerr22010MemberCount
  62  decide
  63
  64theorem kerr22010_event_count_pos : 0 < kerr22010EventCount := by
  65  unfold kerr22010EventCount
  66  decide
  67
  68theorem kerr22010_sample_count_pos : 0 < kerr22010TotalSampleCount := by
  69  unfold kerr22010TotalSampleCount
  70  decide
  71
  72theorem kerr22010_target_above_pooled_95 :
  73    kerr22010PooledQ95 < kerr22010RSDampingTarget := by
  74  unfold kerr22010PooledQ95 kerr22010RSDampingTarget
  75  norm_num
  76
  77theorem kerr22010_target_above_pooled_84 :
  78    kerr22010PooledQ84 < kerr22010RSDampingTarget := by
  79  unfold kerr22010PooledQ84 kerr22010RSDampingTarget
  80  norm_num
  81
  82theorem kerr22010_z_from_mean_gt_two :
  83    2 < kerr22010PooledZFromMean := by
  84  unfold kerr22010PooledZFromMean
  85  norm_num
  86
  87theorem kerr22010_fraction_below_target_valid :
  88    0 < kerr22010PooledFractionBelowTarget ∧ kerr22010PooledFractionBelowTarget < 1 := by
  89  unfold kerr22010PooledFractionBelowTarget
  90  norm_num
  91
  92theorem kerr22010_no_members_inside68 :
  93    kerr22010MembersInside68Count = 0 := rfl
  94
  95theorem kerr22010_mean_lt_kerr2200_mean :
  96    kerr22010PooledMean < kerr2200PooledMean := by
  97  unfold kerr22010PooledMean kerr2200PooledMean
  98  norm_num
  99
 100/-! ## §3. Master cert -/
 101
 102structure GWTC3RingdownKerr22010MDampingFamilyCert where
 103  member_count_pos : 0 < kerr22010MemberCount
 104  event_count_pos : 0 < kerr22010EventCount
 105  sample_count_pos : 0 < kerr22010TotalSampleCount
 106  target_above_pooled_95 : kerr22010PooledQ95 < kerr22010RSDampingTarget
 107  target_above_pooled_84 : kerr22010PooledQ84 < kerr22010RSDampingTarget
 108  z_gt_two : 2 < kerr22010PooledZFromMean
 109  fraction_valid :
 110    0 < kerr22010PooledFractionBelowTarget ∧ kerr22010PooledFractionBelowTarget < 1
 111  no_members_inside68 : kerr22010MembersInside68Count = 0
 112  mean_lt_kerr2200 : kerr22010PooledMean < kerr2200PooledMean
 113  kerr2200_available : Nonempty GWTC3RingdownKerr2200MDampingFamilyCert
 114
 115def gwtc3RingdownKerr22010MDampingFamilyCert :
 116    GWTC3RingdownKerr22010MDampingFamilyCert where
 117  member_count_pos := kerr22010_member_count_pos
 118  event_count_pos := kerr22010_event_count_pos
 119  sample_count_pos := kerr22010_sample_count_pos
 120  target_above_pooled_95 := kerr22010_target_above_pooled_95
 121  target_above_pooled_84 := kerr22010_target_above_pooled_84
 122  z_gt_two := kerr22010_z_from_mean_gt_two
 123  fraction_valid := kerr22010_fraction_below_target_valid
 124  no_members_inside68 := kerr22010_no_members_inside68
 125  mean_lt_kerr2200 := kerr22010_mean_lt_kerr2200_mean
 126  kerr2200_available := gwtc3RingdownKerr2200MDampingFamilyCert_inhabited
 127
 128theorem gwtc3RingdownKerr22010MDampingFamilyCert_inhabited :
 129    Nonempty GWTC3RingdownKerr22010MDampingFamilyCert :=
 130  ⟨gwtc3RingdownKerr22010MDampingFamilyCert⟩
 131
 132/-- One-statement Kerr_220_10M family damping theorem. -/
 133theorem gwtc3_ringdown_kerr22010m_damping_family_one_statement :
 134    (kerr22010MemberCount = 22) ∧
 135    (kerr22010EventCount = 22) ∧
 136    (kerr22010TotalSampleCount = 664154) ∧
 137    (kerr22010PooledQ95 < kerr22010RSDampingTarget) ∧
 138    (2 < kerr22010PooledZFromMean) ∧
 139    (kerr22010MembersInside68Count = 0) ∧
 140    (kerr22010PooledMean < kerr2200PooledMean) ∧
 141    Nonempty GWTC3RingdownKerr22010MDampingFamilyCert :=
 142  ⟨rfl, rfl, rfl,
 143   kerr22010_target_above_pooled_95,
 144   kerr22010_z_from_mean_gt_two,
 145   rfl,
 146   kerr22010_mean_lt_kerr2200_mean,
 147   gwtc3RingdownKerr22010MDampingFamilyCert_inhabited⟩
 148
 149end GWTC3RingdownKerr22010MDampingFamily
 150end Verification
 151end IndisputableMonolith
 152