taxonomyWaveformCount
plain-language theorem explainer
Fixes the waveform-category member count in the GWTC-3 ringdown ZIP filename taxonomy at 18. Cited by anyone checking that Kerr, MMRDNP, damped-sinusoid, and waveform partition the 243 HDF5 files. Bare natural-number definition aligned with the Session-118 central-directory census; no proof obligations.
Claim. In the GWTC-3 ringdown archive filename taxonomy, the number of HDF5 members in the waveform category is $18$.
background
The module records an archive-wide filename taxonomy of the 243 HDF5 files inside IGWN-GWTC3-TGR-v1-rin.zip, using only the ZIP central directory. No posterior samples are opened. Companion Python reproduces the same census.
Live category split is Kerr 159, MMRDNP 44, damped-sinusoid 22, waveform 18. Sibling constants fix the other three category sizes, the two pipeline sizes (pyring 225, pseobnrv4hm 18), event count 26, and total HDF5 count 243. This constant is the waveform cell of that table.
Status is structural: zero sorry, zero new RS-specific axioms. Taxonomy only; no likelihood or TGR test is computed here.
proof idea
Literal definition: the natural number 18. No tactics, no lemmas. Downstream theorems unfold this name and close equalities by decide.
why it matters
Supplies the waveform term in taxonomy_category_sum, which proves Kerr + MMRDNP + damped-sinusoid + waveform equals the HDF5 total. That equality is a field of GWTC3RingdownFilenameTaxonomyCert and appears in the bundled one-statement taxonomy theorem. Without this constant the category partition cannot be stated inside Lean. It is verification scaffolding for GWTC-3 ringdown archive integrity, not a physics derivation step (T0–T8, RCL, or mass ladder).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.