taxonomy_pipeline_sum
plain-language theorem explainer
The two ringdown analysis pipelines in the GWTC-3 TGR ringdown archive partition the full set of 243 HDF5 files: 225 from pyring and 18 from pseobnrv4hm. Anyone citing the archive-wide filename taxonomy would use this identity. The proof unfolds the three natural-number constants and closes by decidable arithmetic.
Claim. The pyring pipeline count plus the pseobnrv4hm pipeline count equals the total HDF5 file count in the GWTC-3 ringdown archive: $225 + 18 = 243$.
background
This module records a pure filename taxonomy of the 243 HDF5 members of IGWN-GWTC3-TGR-v1-rin.zip, taken only from the ZIP central directory. No posterior samples are opened. The live counts are: 26 events; pipelines pyring = 225 and pseobnrv4hm = 18; categories Kerr = 159, MMRDNP = 44, damped-sinusoid = 22, waveform = 18.
The three constants used here are literal Nat definitions: total HDF5 files = 243, pyring files = 225, pseobnrv4hm files = 18. They are the pipeline slice of that taxonomy. Companion script gwtc3_ringdown_filename_taxonomy.py regenerates the same numbers from the archive listing.
proof idea
Term-mode proof by unfolding the three Nat definitions to the literals 225, 18, and 243, then closing with decide on the ground equality $225 + 18 = 243$. No lemmas beyond decidable natural arithmetic are required.
why it matters
This identity is the pipeline_sum field of gwtc3RingdownFilenameTaxonomyCert, the module-level certificate that packages the archive taxonomy. Together with the category-sum and ZIP-schema match lemmas, it shows the filename partition is exhaustive and consistent with the ZIP central directory. The result is structural verification only: taxonomy closure with zero sorry and no RS-internal axioms. It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it anchors the GWTC-3 ringdown data surface used by later verification claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.