IndisputableMonolith.Verification.GWTC3RingdownFamilyComparison

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily
   3import IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily
   4import IndisputableMonolith.Verification.GWTC3RingdownKerr22010MDampingFamily
   5
   6/-!
   7# GWTC-3 Ringdown Controlled-Family Comparison
   8
   9## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
  10
  11This module aggregates the three currently mapped damping families:
  12
  13* `DS_1mode_10M`
  14* `Kerr_220_0M`
  15* `Kerr_220_10M`
  16
  17and proves the model/start-time dependence facts:
  18
  19* mean order: `DS_1mode_10M > Kerr_220_0M > Kerr_220_10M`
  20* median order: `DS_1mode_10M > Kerr_220_0M > Kerr_220_10M`
  21* target inclusion degrades across the same order:
  22  - DS: target in pooled 68% and 90%
  23  - Kerr_220_0M: target in pooled 90% only
  24  - Kerr_220_10M: target in neither pooled 68% nor 90%
  25
  26This is a three-family comparison only, not a mixed-model archive-wide
  27likelihood.
  28Zero `sorry`. Zero new RS-specific axioms.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Verification
  33namespace GWTC3RingdownFamilyComparison
  34
  35open IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily
  36open IndisputableMonolith.Verification.GWTC3RingdownKerr2200MDampingFamily
  37open IndisputableMonolith.Verification.GWTC3RingdownKerr22010MDampingFamily
  38
  39/-! ## §1. Comparison constants -/
  40
  41def comparisonFamilyCount : Nat := 3
  42def comparisonTotalMembers : Nat := 66
  43def comparisonTotalSamples : Nat := 1954998
  44def dsMeanMinusKerr0Mean : ℝ := 0.143049219914
  45def kerr0MeanMinusKerr10Mean : ℝ := 0.089478304903
  46def dsHitDiffVsKerr0 : Nat := 10
  47def kerr0HitDiffVsKerr10 : Nat := 3
  48
  49/-! ## §2. Ordering facts -/
  50
  51theorem comparison_total_members :
  52    dsFamilyMemberCount + kerr2200MemberCount + kerr22010MemberCount =
  53      comparisonTotalMembers := by
  54  unfold dsFamilyMemberCount kerr2200MemberCount kerr22010MemberCount comparisonTotalMembers
  55  decide
  56
  57theorem comparison_total_samples :
  58    dsFamilyTotalSampleCount + kerr2200TotalSampleCount + kerr22010TotalSampleCount =
  59      comparisonTotalSamples := by
  60  unfold dsFamilyTotalSampleCount kerr2200TotalSampleCount kerr22010TotalSampleCount
  61    comparisonTotalSamples
  62  decide
  63
  64theorem family_mean_order :
  65    kerr22010PooledMean < kerr2200PooledMean ∧
  66      kerr2200PooledMean < dsPooledMean := by
  67  exact ⟨kerr22010_mean_lt_kerr2200_mean, ds_vs_kerr_mean_order⟩
  68
  69theorem family_median_order :
  70    kerr22010PooledMedian < kerr2200PooledMedian ∧
  71      kerr2200PooledMedian < dsPooledMedian := by
  72  unfold kerr22010PooledMedian kerr2200PooledMedian dsPooledMedian
  73  norm_num
  74
  75theorem hit_count_order :
  76    kerr22010MembersInside68Count < kerr2200MembersInside68Count ∧
  77      kerr2200MembersInside68Count < dsMembersInside68Count := by
  78  unfold kerr22010MembersInside68Count kerr2200MembersInside68Count dsMembersInside68Count
  79  decide
  80
  81theorem ds_mean_difference_pos :
  82    0 < dsMeanMinusKerr0Mean := by
  83  unfold dsMeanMinusKerr0Mean
  84  norm_num
  85
  86theorem kerr_mean_difference_pos :
  87    0 < kerr0MeanMinusKerr10Mean := by
  88  unfold kerr0MeanMinusKerr10Mean
  89  norm_num
  90
  91/-! ## §3. Master cert -/
  92
  93structure GWTC3RingdownFamilyComparisonCert where
  94  total_members :
  95    dsFamilyMemberCount + kerr2200MemberCount + kerr22010MemberCount =
  96      comparisonTotalMembers
  97  total_samples :
  98    dsFamilyTotalSampleCount + kerr2200TotalSampleCount + kerr22010TotalSampleCount =
  99      comparisonTotalSamples
 100  mean_order :
 101    kerr22010PooledMean < kerr2200PooledMean ∧
 102      kerr2200PooledMean < dsPooledMean
 103  median_order :
 104    kerr22010PooledMedian < kerr2200PooledMedian ∧
 105      kerr2200PooledMedian < dsPooledMedian
 106  hit_order :
 107    kerr22010MembersInside68Count < kerr2200MembersInside68Count ∧
 108      kerr2200MembersInside68Count < dsMembersInside68Count
 109  ds_available : Nonempty GWTC3RingdownDS1Mode10MDampingFamilyCert
 110  kerr0_available : Nonempty GWTC3RingdownKerr2200MDampingFamilyCert
 111  kerr10_available : Nonempty GWTC3RingdownKerr22010MDampingFamilyCert
 112
 113def gwtc3RingdownFamilyComparisonCert :
 114    GWTC3RingdownFamilyComparisonCert where
 115  total_members := comparison_total_members
 116  total_samples := comparison_total_samples
 117  mean_order := family_mean_order
 118  median_order := family_median_order
 119  hit_order := hit_count_order
 120  ds_available := gwtc3RingdownDS1Mode10MDampingFamilyCert_inhabited
 121  kerr0_available := gwtc3RingdownKerr2200MDampingFamilyCert_inhabited
 122  kerr10_available := gwtc3RingdownKerr22010MDampingFamilyCert_inhabited
 123
 124theorem gwtc3RingdownFamilyComparisonCert_inhabited :
 125    Nonempty GWTC3RingdownFamilyComparisonCert :=
 126  ⟨gwtc3RingdownFamilyComparisonCert⟩
 127
 128/-- One-statement controlled-family comparison theorem. -/
 129theorem gwtc3_ringdown_family_comparison_one_statement :
 130    (comparisonFamilyCount = 3) ∧
 131    (comparisonTotalMembers = 66) ∧
 132    (comparisonTotalSamples = 1954998) ∧
 133    (kerr22010PooledMean < kerr2200PooledMean ∧
 134      kerr2200PooledMean < dsPooledMean) ∧
 135    (kerr22010PooledMedian < kerr2200PooledMedian ∧
 136      kerr2200PooledMedian < dsPooledMedian) ∧
 137    (kerr22010MembersInside68Count < kerr2200MembersInside68Count ∧
 138      kerr2200MembersInside68Count < dsMembersInside68Count) ∧
 139    Nonempty GWTC3RingdownFamilyComparisonCert :=
 140  ⟨rfl, rfl, rfl,
 141   family_mean_order,
 142   family_median_order,
 143   hit_count_order,
 144   gwtc3RingdownFamilyComparisonCert_inhabited⟩
 145
 146end GWTC3RingdownFamilyComparison
 147end Verification
 148end IndisputableMonolith
 149