IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSchema
   3
   4/-!
   5# GWTC-3 Ringdown HDF5 Sample Summary
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9This module records the first posterior-summary statistics extracted
  10from a range-read GWTC-3 ringdown HDF5 file:
  11
  12* member: `rin/rin_S190727h_pyring_DS_1mode_10M.h5`
  13* dataset: `/EXP6/posterior_samples`
  14* sample count: `15114`
  15* field count: `7`
  16* fields: `psi`, `logA_t_0`, `f_t_0`, `tau_t_0`, `phi_t_0`, `logL`, `logPrior`
  17
  18Companion script:
  19
  20* `papers/reproducibility/gwtc3_ringdown_hdf5_sample_summary.py`
  21
  22This is one-member posterior summary only, not an RS echo/QNM
  23likelihood. The purpose is to establish the column names and basic
  24numerical ranges needed by the later likelihood parser.
  25
  26Zero `sorry`. Zero new RS-specific axioms.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Verification
  31namespace GWTC3RingdownHDF5SampleSummary
  32
  33open IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSchema
  34
  35/-! ## §1. Summary constants -/
  36
  37def summaryMemberName : String := "rin/rin_S190727h_pyring_DS_1mode_10M.h5"
  38def summaryPosteriorPath : String := "/EXP6/posterior_samples"
  39def summarySampleCount : Nat := 15114
  40def summaryFieldCount : Nat := 7
  41
  42def psiMean : ℝ := 1.5465191
  43def logAMean : ℝ := -22.244585
  44def fMean : ℝ := 420.95381
  45def tauMean : ℝ := 0.022773848
  46def phiMean : ℝ := 3.1523706
  47def logLMean : ℝ := 58695.535
  48def logPriorMean : ℝ := 0
  49
  50def fQ16 : ℝ := 172.53798
  51def fMedian : ℝ := 345.41413
  52def fQ84 : ℝ := 819.88387
  53
  54def tauQ16 : ℝ := 0.0076396112
  55def tauMedian : ℝ := 0.021072448
  56def tauQ84 : ℝ := 0.039327675
  57
  58/-! ## §2. Basic schema and sign facts -/
  59
  60theorem summary_member_matches_schema :
  61    summaryMemberName = sampleMemberName := rfl
  62
  63theorem summary_path_matches_schema :
  64    summaryPosteriorPath = posteriorSamplesDatasetPath := rfl
  65
  66theorem summary_sample_count_matches_schema :
  67    summarySampleCount = posteriorSamplesCount := rfl
  68
  69theorem summary_field_count_matches_schema :
  70    summaryFieldCount = posteriorFieldCount := rfl
  71
  72theorem summary_sample_count_pos : 0 < summarySampleCount := by
  73  unfold summarySampleCount
  74  decide
  75
  76theorem summary_field_count_pos : 0 < summaryFieldCount := by
  77  unfold summaryFieldCount
  78  decide
  79
  80theorem mean_signs :
  81    0 < psiMean ∧ logAMean < 0 ∧ 0 < fMean ∧ 0 < tauMean ∧
  82      0 < phiMean ∧ 0 < logLMean ∧ logPriorMean = 0 := by
  83  unfold psiMean logAMean fMean tauMean phiMean logLMean logPriorMean
  84  norm_num
  85
  86theorem f_quantile_order :
  87    fQ16 < fMedian ∧ fMedian < fQ84 := by
  88  unfold fQ16 fMedian fQ84
  89  norm_num
  90
  91theorem tau_quantile_order :
  92    tauQ16 < tauMedian ∧ tauMedian < tauQ84 := by
  93  unfold tauQ16 tauMedian tauQ84
  94  norm_num
  95
  96/-! ## §3. Master cert -/
  97
  98structure GWTC3RingdownHDF5SampleSummaryCert where
  99  member_matches_schema : summaryMemberName = sampleMemberName
 100  path_matches_schema : summaryPosteriorPath = posteriorSamplesDatasetPath
 101  sample_count_matches_schema : summarySampleCount = posteriorSamplesCount
 102  field_count_matches_schema : summaryFieldCount = posteriorFieldCount
 103  sample_count_pos : 0 < summarySampleCount
 104  field_count_pos : 0 < summaryFieldCount
 105  signs :
 106    0 < psiMean ∧ logAMean < 0 ∧ 0 < fMean ∧ 0 < tauMean ∧
 107      0 < phiMean ∧ 0 < logLMean ∧ logPriorMean = 0
 108  f_quantiles : fQ16 < fMedian ∧ fMedian < fQ84
 109  tau_quantiles : tauQ16 < tauMedian ∧ tauMedian < tauQ84
 110  schema_cert_available : Nonempty GWTC3RingdownHDF5SampleSchemaCert
 111
 112def gwtc3RingdownHDF5SampleSummaryCert :
 113    GWTC3RingdownHDF5SampleSummaryCert where
 114  member_matches_schema := summary_member_matches_schema
 115  path_matches_schema := summary_path_matches_schema
 116  sample_count_matches_schema := summary_sample_count_matches_schema
 117  field_count_matches_schema := summary_field_count_matches_schema
 118  sample_count_pos := summary_sample_count_pos
 119  field_count_pos := summary_field_count_pos
 120  signs := mean_signs
 121  f_quantiles := f_quantile_order
 122  tau_quantiles := tau_quantile_order
 123  schema_cert_available := gwtc3RingdownHDF5SampleSchemaCert_inhabited
 124
 125theorem gwtc3RingdownHDF5SampleSummaryCert_inhabited :
 126    Nonempty GWTC3RingdownHDF5SampleSummaryCert :=
 127  ⟨gwtc3RingdownHDF5SampleSummaryCert⟩
 128
 129/-- One-statement posterior-summary theorem for the range-read HDF5 sample. -/
 130theorem gwtc3_ringdown_hdf5_sample_summary_one_statement :
 131    (summarySampleCount = 15114) ∧
 132    (summaryFieldCount = 7) ∧
 133    (0 < fMean) ∧
 134    (0 < tauMean) ∧
 135    (logAMean < 0) ∧
 136    (logPriorMean = 0) ∧
 137    (fQ16 < fMedian ∧ fMedian < fQ84) ∧
 138    (tauQ16 < tauMedian ∧ tauMedian < tauQ84) ∧
 139    Nonempty GWTC3RingdownHDF5SampleSummaryCert :=
 140  ⟨rfl, rfl,
 141   mean_signs.2.2.1,
 142   mean_signs.2.2.2.1,
 143   mean_signs.2.1,
 144   mean_signs.2.2.2.2.2.2,
 145   f_quantile_order,
 146   tau_quantile_order,
 147   gwtc3RingdownHDF5SampleSummaryCert_inhabited⟩
 148
 149end GWTC3RingdownHDF5SampleSummary
 150end Verification
 151end IndisputableMonolith
 152