taxonomyEventCount
plain-language theorem explainer
Fixes the GWTC-3 ringdown archive event count at 26, read from ZIP central-directory filenames only. Anyone citing the structural taxonomy certificate or the one-statement filename theorem uses this constant. It is a bare Nat definition, not a derived proof.
Claim. The number of distinct gravitational-wave events appearing in the GWTC-3 ringdown filename taxonomy is $26$.
background
The module freezes an archive-wide filename taxonomy for the 243 HDF5 members of IGWN-GWTC3-TGR-v1-rin.zip, using only the ZIP central directory. No posterior samples are opened. Companion Python reproduces the same counts.
Live taxonomy figures include 26 events, two pipelines (pyring 225, pseobnrv4hm 18), and four analysis categories (Kerr, MMRDNP, damped-sinusoid, waveform). Sibling constants record those other tallies and the extreme member sizes. Status is structural: zero sorry, zero new RS axioms.
This constant is the event leg of that census. It sits beside the HDF5 file count and the pipeline/category counters that the certificate later sums.
proof idea
Literal definition: the natural number 26. No lemmas, tactics, or computation. Downstream positivity unfolds the definition and closes by decide.
why it matters
Supplies the event count that the one-statement taxonomy theorem conjoins with the HDF5, pipeline, and category equalities, and that the certificate structure packages for verification consumers. Also feeds the elementary positivity lemma 0 < taxonomyEventCount. The module is taxonomy-only infrastructure for GWTC-3 ringdown reproducibility; it does not touch Recognition forcing (T0–T8), J-cost, or mass ladders. It closes a structural audit path: filename census matches the published ZIP layout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.