Verification Gwtc3 Ringdown Filename Taxonomy

The archive census

The GWTC-3 ringdown filename taxonomy is a formal inventory of the 243 HDF5 files inside the public archive IGWN-GWTC3-TGR-v1-rin.zip, a collection of gravitational-wave ringdown analyses from the LIGO-Virgo-KAGRA collaboration's third observing run. The inventory records only what the ZIP central directory says: how many files exist, which events they belong to, which analysis pipeline produced each one, and which physical category each filename encodes. It reads no posterior samples and computes no likelihoods; it is a census of names, not a measurement of physics.

The census counts 26 events, split between two pipelines: 225 files from pyring and 18 from pseobnrv4hm. By category, 159 files are Kerr ringdowns, 44 are labeled MMRDNP, 22 are damped sinusoids, and 18 are waveforms. The smallest member is rin/rin_S190727h_pyring_DS_1mode_10M.h5; the largest is rin/rin_S191109d_pseobnrv4hm.h5. The compressed archive holds about 1.44 gigabytes, expanding to about 1.96 gigabytes uncompressed.

In Recognition Science, the framework's machine-checked library of formal theorems records this taxonomy as a structural theorem: a statement about the archive's shape, not about its scientific content. The library defines each count as a constant, then proves the counts are consistent. The two pipeline counts sum to 243, the four category counts sum to 243, the file count matches the ZIP schema's own count, and the compressed size is provably smaller than the uncompressed size. These are checked by computation, with zero unproved assumptions and zero gaps.

The master certificate bundles all these identities into one object, and a one-statement theorem packages the headline numbers: 243 files, 26 events, 225 pyring files, 18 pseobnrv4hm files, categories that sum correctly, and a certificate that everything is inhabited. The point is reproducibility: a future reader can verify the archive's structure without trusting a human transcript, because the counts and their arithmetic are machine-checked. This establishes what the archive contains, in a form that cannot silently drift from the actual ZIP file.

theorem taxonomy_pipeline_sum :
    taxonomyPyringCount + taxonomyPSEOBNRv4HMCount = taxonomyHDF5FileCount := by
  unfold taxonomyPyringCount taxonomyPSEOBNRv4HMCount taxonomyHDF5FileCount
  decide

theorem taxonomy_pipeline_sum :
    taxonomyPyringCount + taxonomyPSEOBNRv4HMCount = taxonomyHDF5FileCount := by
  unfold taxonomyPyringCount taxonomyPSEOBNRv4HMCount taxonomyHDF5FileCount
  decide

theorem taxonomy_category_sum :
    taxonomyKerrCount + taxonomyMMRDNPCount + taxonomyDampedSinusoidCount +
      taxonomyWaveformCount = taxonomyHDF5FileCount := by
  unfold taxonomyKerrCount taxonomyMMRDNPCount taxonomyDampedSinusoidCount
    taxonomyWaveformCount taxonomyHDF5FileCount
  decide

theorem taxonomy_hdf5_count_matches_zip_schema :
    taxonomyHDF5FileCount = ringdownZipH5Count := rfl

theorem taxonomy_uncompressed_gt_compressed :
    taxonomyTotalCompressedSize < taxonomyTotalUncompressedSize := by
  unfold taxonomyTotalCompressedSize taxonomyTotalUncompressedSize
  decide

def gwtc3RingdownFilenameTaxonomyCert :
    GWTC3RingdownFilenameTaxonomyCert where
  pipeline_sum := taxonomy_pipeline_sum
  category_sum := taxonomy_category_sum
  hdf5_count_matches_zip := taxonomy_hdf5_count_matches_zip_schema
  compressed_matches_zip := taxonomy_total_compressed_matches_zip_schema
  uncompressed_matches_zip := taxonomy_total_uncompressed_matches_zip_schema
  uncompressed_gt_compressed := taxonomy_uncompressed_gt_compressed
  event_count_pos := taxonomy_event_count_pos
  smallest_named := taxonomy_smallest_member_named
  largest_named := taxonomy_largest_member_named
  zip_schema_available := gwtc3RingdownZipSchemaCert_inhabited

/-- One-statement filename-taxonomy theorem. -/
theorem gwtc3_ringdown_filename_taxonomy_one_statement :
    (taxonomyHDF5FileCount = 243) ∧
    (taxonomyEventCount = 26) ∧
    (taxonomyPyringCount = 225) ∧
    (taxonomyPSEOBNRv4HMCount = 18) ∧
    (taxonomyKerrCount + taxonomyMMRDNPCount + taxonomyDampedSinusoidCount +
      taxonomyWaveformCount = taxonomyHDF5FileCount) ∧
    Nonempty GWTC3RingdownFilenameTaxonomyCert :=
  ⟨rfl, rfl, rfl, rfl, taxonomy_category_sum,
   gwtc3RingdownFilenameTaxonomyCert_inhabited⟩

What this page does not claim

No posterior sample or likelihood value is read or verified. No claim is made about the scientific validity of the ringdown analyses themselves. The taxonomy does not derive any physical constant or recognition-theoretic result.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/GWTC3RingdownFilenameTaxonomy.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: