IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy

   1import Mathlib
   2import IndisputableMonolith.Verification.GWTC3RingdownZipSchema
   3
   4/-!
   5# GWTC-3 Ringdown Filename Taxonomy
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   8
   9This module records the archive-wide filename taxonomy of the 243 HDF5
  10files in `IGWN-GWTC3-TGR-v1-rin.zip`, using only the ZIP central
  11directory from Session 118. No posterior samples are read.
  12
  13Companion script:
  14
  15* `papers/reproducibility/gwtc3_ringdown_filename_taxonomy.py`
  16
  17Live taxonomy:
  18
  19* HDF5 files: `243`
  20* Events: `26`
  21* Pipelines: `pyring = 225`, `pseobnrv4hm = 18`
  22* Categories: `Kerr = 159`, `MMRDNP = 44`, `damped-sinusoid = 22`,
  23  `waveform = 18`
  24* Smallest member:
  25  `rin/rin_S190727h_pyring_DS_1mode_10M.h5`
  26* Largest member:
  27  `rin/rin_S191109d_pseobnrv4hm.h5`
  28
  29This is taxonomy only. No posterior likelihood is computed.
  30Zero `sorry`. Zero new RS-specific axioms.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Verification
  35namespace GWTC3RingdownFilenameTaxonomy
  36
  37open IndisputableMonolith.Verification.GWTC3RingdownZipSchema
  38
  39/-! ## §1. Taxonomy constants -/
  40
  41def taxonomyHDF5FileCount : Nat := 243
  42def taxonomyEventCount : Nat := 26
  43def taxonomyPyringCount : Nat := 225
  44def taxonomyPSEOBNRv4HMCount : Nat := 18
  45def taxonomyKerrCount : Nat := 159
  46def taxonomyMMRDNPCount : Nat := 44
  47def taxonomyDampedSinusoidCount : Nat := 22
  48def taxonomyWaveformCount : Nat := 18
  49def taxonomyTotalCompressedSize : Nat := 1444151741
  50def taxonomyTotalUncompressedSize : Nat := 1963931876
  51def taxonomySmallestMember : String := "rin/rin_S190727h_pyring_DS_1mode_10M.h5"
  52def taxonomyLargestMember : String := "rin/rin_S191109d_pseobnrv4hm.h5"
  53
  54/-! ## §2. Count identities -/
  55
  56theorem taxonomy_pipeline_sum :
  57    taxonomyPyringCount + taxonomyPSEOBNRv4HMCount = taxonomyHDF5FileCount := by
  58  unfold taxonomyPyringCount taxonomyPSEOBNRv4HMCount taxonomyHDF5FileCount
  59  decide
  60
  61theorem taxonomy_category_sum :
  62    taxonomyKerrCount + taxonomyMMRDNPCount + taxonomyDampedSinusoidCount +
  63      taxonomyWaveformCount = taxonomyHDF5FileCount := by
  64  unfold taxonomyKerrCount taxonomyMMRDNPCount taxonomyDampedSinusoidCount
  65    taxonomyWaveformCount taxonomyHDF5FileCount
  66  decide
  67
  68theorem taxonomy_hdf5_count_matches_zip_schema :
  69    taxonomyHDF5FileCount = ringdownZipH5Count := rfl
  70
  71theorem taxonomy_total_compressed_matches_zip_schema :
  72    taxonomyTotalCompressedSize = ringdownZipTotalCompressedSize := rfl
  73
  74theorem taxonomy_total_uncompressed_matches_zip_schema :
  75    taxonomyTotalUncompressedSize = ringdownZipTotalUncompressedSize := rfl
  76
  77theorem taxonomy_uncompressed_gt_compressed :
  78    taxonomyTotalCompressedSize < taxonomyTotalUncompressedSize := by
  79  unfold taxonomyTotalCompressedSize taxonomyTotalUncompressedSize
  80  decide
  81
  82theorem taxonomy_event_count_pos : 0 < taxonomyEventCount := by
  83  unfold taxonomyEventCount
  84  decide
  85
  86theorem taxonomy_smallest_member_named :
  87    taxonomySmallestMember = "rin/rin_S190727h_pyring_DS_1mode_10M.h5" := rfl
  88
  89theorem taxonomy_largest_member_named :
  90    taxonomyLargestMember = "rin/rin_S191109d_pseobnrv4hm.h5" := rfl
  91
  92/-! ## §3. Master cert -/
  93
  94structure GWTC3RingdownFilenameTaxonomyCert where
  95  pipeline_sum : taxonomyPyringCount + taxonomyPSEOBNRv4HMCount = taxonomyHDF5FileCount
  96  category_sum :
  97    taxonomyKerrCount + taxonomyMMRDNPCount + taxonomyDampedSinusoidCount +
  98      taxonomyWaveformCount = taxonomyHDF5FileCount
  99  hdf5_count_matches_zip : taxonomyHDF5FileCount = ringdownZipH5Count
 100  compressed_matches_zip : taxonomyTotalCompressedSize = ringdownZipTotalCompressedSize
 101  uncompressed_matches_zip : taxonomyTotalUncompressedSize = ringdownZipTotalUncompressedSize
 102  uncompressed_gt_compressed : taxonomyTotalCompressedSize < taxonomyTotalUncompressedSize
 103  event_count_pos : 0 < taxonomyEventCount
 104  smallest_named :
 105    taxonomySmallestMember = "rin/rin_S190727h_pyring_DS_1mode_10M.h5"
 106  largest_named :
 107    taxonomyLargestMember = "rin/rin_S191109d_pseobnrv4hm.h5"
 108  zip_schema_available : Nonempty GWTC3RingdownZipSchemaCert
 109
 110def gwtc3RingdownFilenameTaxonomyCert :
 111    GWTC3RingdownFilenameTaxonomyCert where
 112  pipeline_sum := taxonomy_pipeline_sum
 113  category_sum := taxonomy_category_sum
 114  hdf5_count_matches_zip := taxonomy_hdf5_count_matches_zip_schema
 115  compressed_matches_zip := taxonomy_total_compressed_matches_zip_schema
 116  uncompressed_matches_zip := taxonomy_total_uncompressed_matches_zip_schema
 117  uncompressed_gt_compressed := taxonomy_uncompressed_gt_compressed
 118  event_count_pos := taxonomy_event_count_pos
 119  smallest_named := taxonomy_smallest_member_named
 120  largest_named := taxonomy_largest_member_named
 121  zip_schema_available := gwtc3RingdownZipSchemaCert_inhabited
 122
 123theorem gwtc3RingdownFilenameTaxonomyCert_inhabited :
 124    Nonempty GWTC3RingdownFilenameTaxonomyCert :=
 125  ⟨gwtc3RingdownFilenameTaxonomyCert⟩
 126
 127/-- One-statement filename-taxonomy theorem. -/
 128theorem gwtc3_ringdown_filename_taxonomy_one_statement :
 129    (taxonomyHDF5FileCount = 243) ∧
 130    (taxonomyEventCount = 26) ∧
 131    (taxonomyPyringCount = 225) ∧
 132    (taxonomyPSEOBNRv4HMCount = 18) ∧
 133    (taxonomyKerrCount + taxonomyMMRDNPCount + taxonomyDampedSinusoidCount +
 134      taxonomyWaveformCount = taxonomyHDF5FileCount) ∧
 135    Nonempty GWTC3RingdownFilenameTaxonomyCert :=
 136  ⟨rfl, rfl, rfl, rfl, taxonomy_category_sum,
 137   gwtc3RingdownFilenameTaxonomyCert_inhabited⟩
 138
 139end GWTC3RingdownFilenameTaxonomy
 140end Verification
 141end IndisputableMonolith
 142