taxonomyKerrCount
plain-language theorem explainer
Fixes the Kerr-category count at 159 among the 243 GWTC-3 ringdown HDF5 files. Anyone checking the archive filename taxonomy or the category-sum identity cites this constant. It is a bare natural-number definition, not a derived theorem.
Claim. The number of GWTC-3 ringdown HDF5 members classified under the Kerr filename category is $159$.
background
The module freezes the archive-wide filename taxonomy of IGWN-GWTC3-TGR-v1-rin.zip from the ZIP central directory alone. No posterior samples are opened. The live counts are 243 HDF5 files, 26 events, two pipelines (pyring 225, pseobnrv4hm 18), and four analysis categories: Kerr 159, MMRDNP 44, damped-sinusoid 22, waveform 18.
Sibling constants record the other category sizes and the pipeline split. The Kerr count is the largest single category and is the first summand in the category partition of the full file list. Companion Python under papers/reproducibility/ regenerates the same numbers from the ZIP index.
proof idea
No proof. The declaration is a definitional abbreviation of the natural number 159, matching the external taxonomy script and the module header. Downstream equalities unfold this constant and discharge arithmetic by decide.
why it matters
Supplies the Kerr summand for taxonomy_category_sum, which proves Kerr + MMRDNP + damped-sinusoid + waveform equals the HDF5 total. That identity is a field of GWTC3RingdownFilenameTaxonomyCert and appears in the conjunctive one-statement taxonomy theorem. The module is structural verification only: zero sorry, zero new RS axioms, and no likelihood or mass-ladder content. It anchors the GWTC-3 ringdown archive inventory used by later verification certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.