IndisputableMonolith.Verification.GWTC3RingdownOneMemberRSStatistic

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary
   3
   4/-!
   5# GWTC-3 Ringdown One-Member RS Amplitude Statistic
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9This module records the first explicitly RS-referenced statistic on a
  10range-read GWTC-3 ringdown posterior table.
  11
  12Member:
  13
  14* `rin/rin_S190727h_pyring_DS_1mode_10M.h5`
  15
  16Dataset:
  17
  18* `/EXP6/posterior_samples`
  19
  20Column:
  21
  22* `logA_t_0`
  23
  24RS structural target:
  25
  26* `log(φ^-44) = -44 log φ ≈ -21.173320302623`
  27
  28Result:
  29
  30* posterior mean `logA_t_0 ≈ -22.244585483768`
  31* posterior std `≈ 0.398295292686`
  32* posterior median `≈ -22.211884808706`
  33* target is not inside the central 90% or 68% posterior intervals
  34* target is about `2.689626` posterior std above the mean
  35* sample fraction above target is `0.000331`
  36
  37This is one-member amplitude-scale comparison only. It does not prove
  38that `logA_t_0` is the final RS echo amplitude observable, and it does
  39not compute an archive-wide likelihood.
  40
  41Zero `sorry`. Zero new RS-specific axioms.
  42-/
  43
  44namespace IndisputableMonolith
  45namespace Verification
  46namespace GWTC3RingdownOneMemberRSStatistic
  47
  48open IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary
  49
  50/-! ## §1. Statistic constants -/
  51
  52def rsLogPhiNeg44Target : ℝ := -21.173320302623
  53def logAPosteriorMean : ℝ := -22.244585483768
  54def logAPosteriorStd : ℝ := 0.398295292686
  55def logAPosteriorMedian : ℝ := -22.211884808706
  56def logAQ05 : ℝ := -22.911300360855
  57def logAQ16 : ℝ := -22.719806844144
  58def logAQ84 : ℝ := -21.824897151633
  59def logAQ95 : ℝ := -21.638354687882
  60def logAResidualFromMean : ℝ := 1.071265181145
  61def logAResidualFromMedian : ℝ := 1.038564506083
  62def logAZFromMean : ℝ := 2.689626
  63def logAFractionAboveTarget : ℝ := 0.000331
  64
  65/-! ## §2. Basic inequalities -/
  66
  67theorem target_above_q95 :
  68    logAQ95 < rsLogPhiNeg44Target := by
  69  unfold logAQ95 rsLogPhiNeg44Target
  70  norm_num
  71
  72theorem target_outside_90_interval :
  73    ¬ (logAQ05 ≤ rsLogPhiNeg44Target ∧ rsLogPhiNeg44Target ≤ logAQ95) := by
  74  intro h
  75  have hlt := target_above_q95
  76  linarith
  77
  78theorem target_outside_68_interval :
  79    ¬ (logAQ16 ≤ rsLogPhiNeg44Target ∧ rsLogPhiNeg44Target ≤ logAQ84) := by
  80  intro h
  81  unfold logAQ84 rsLogPhiNeg44Target at h
  82  norm_num at h
  83
  84theorem z_from_mean_gt_two :
  85    2 < logAZFromMean := by
  86  unfold logAZFromMean
  87  norm_num
  88
  89theorem fraction_above_target_small :
  90    logAFractionAboveTarget < 0.001 := by
  91  unfold logAFractionAboveTarget
  92  norm_num
  93
  94theorem posterior_summary_available :
  95    Nonempty GWTC3RingdownHDF5SampleSummaryCert :=
  96  gwtc3RingdownHDF5SampleSummaryCert_inhabited
  97
  98/-! ## §3. Master cert -/
  99
 100structure GWTC3RingdownOneMemberRSStatisticCert where
 101  target_above_q95 : logAQ95 < rsLogPhiNeg44Target
 102  target_outside_90 :
 103    ¬ (logAQ05 ≤ rsLogPhiNeg44Target ∧ rsLogPhiNeg44Target ≤ logAQ95)
 104  target_outside_68 :
 105    ¬ (logAQ16 ≤ rsLogPhiNeg44Target ∧ rsLogPhiNeg44Target ≤ logAQ84)
 106  z_gt_two : 2 < logAZFromMean
 107  fraction_small : logAFractionAboveTarget < 0.001
 108  summary_available : Nonempty GWTC3RingdownHDF5SampleSummaryCert
 109
 110def gwtc3RingdownOneMemberRSStatisticCert :
 111    GWTC3RingdownOneMemberRSStatisticCert where
 112  target_above_q95 := target_above_q95
 113  target_outside_90 := target_outside_90_interval
 114  target_outside_68 := target_outside_68_interval
 115  z_gt_two := z_from_mean_gt_two
 116  fraction_small := fraction_above_target_small
 117  summary_available := posterior_summary_available
 118
 119theorem gwtc3RingdownOneMemberRSStatisticCert_inhabited :
 120    Nonempty GWTC3RingdownOneMemberRSStatisticCert :=
 121  ⟨gwtc3RingdownOneMemberRSStatisticCert⟩
 122
 123/-- One-statement theorem for the one-member RS amplitude-scale statistic. -/
 124theorem gwtc3_ringdown_one_member_rs_statistic_one_statement :
 125    (logAQ95 < rsLogPhiNeg44Target) ∧
 126    (2 < logAZFromMean) ∧
 127    (logAFractionAboveTarget < 0.001) ∧
 128    Nonempty GWTC3RingdownOneMemberRSStatisticCert :=
 129  ⟨target_above_q95,
 130   z_from_mean_gt_two,
 131   fraction_above_target_small,
 132   gwtc3RingdownOneMemberRSStatisticCert_inhabited⟩
 133
 134end GWTC3RingdownOneMemberRSStatistic
 135end Verification
 136end IndisputableMonolith
 137