taxonomyDampedSinusoidCount
plain-language theorem explainer
Records that the GWTC-3 ringdown ZIP archive contains exactly 22 HDF5 members whose filenames fall in the damped-sinusoid category. Citation target for archive-level taxonomy certificates and for the DS 1-mode 10M damping-family count match. The value is a literal natural-number definition, not a derived proof.
Claim. The GWTC-3 ringdown filename taxonomy assigns the damped-sinusoid category the count $22$.
background
The module freezes the archive-wide filename taxonomy of the 243 HDF5 files in IGWN-GWTC3-TGR-v1-rin.zip, read only from the ZIP central directory. No posterior samples are opened. Companion Python reproduces the same counts.
Live taxonomy splits those files by pipeline (pyring 225, pseobnrv4hm 18) and by analysis category: Kerr 159, MMRDNP 44, damped-sinusoid 22, waveform 18. The damped-sinusoid bucket is the count this definition pins.
Sibling constants fix the other category and pipeline tallies, total compressed/uncompressed sizes, and extremal members. The setting is structural verification only: taxonomy closure with zero sorry and no new RS axioms.
proof idea
There is no proof body. The declaration is a bare Nat definition equal to the literal 22, matching the live taxonomy line for the damped-sinusoid category. Downstream equalities (category sum, DS-family member count) discharge by unfold plus decide or by rfl against this constant.
why it matters
Feeds the category-partition identity: Kerr + MMRDNP + damped-sinusoid + waveform equals the 243 HDF5 files, used inside GWTC3RingdownFilenameTaxonomyCert and the one-statement taxonomy theorem. Also anchors ds_family_member_count_matches_taxonomy, which equates the DS 1-mode 10M damping-family member count to this constant, and the corresponding family certificate field.
In the Verification domain this is ledger hygiene for GWTC-3 ringdown reproducibility: a single named count that every later certificate can cite without re-parsing the ZIP. It does not touch RS forcing (T0–T8), RCL, or mass-ladder physics; it only stabilizes the observational archive slice those checks may later consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.