GWTC3RingdownFilenameTaxonomyCert
plain-language theorem explainer
Certificate structure bundling the archive-wide filename taxonomy of the 243 GWTC-3 ringdown HDF5 files: pipeline and category partitions, ZIP size/count matches, positive event count, and named extremal members. Downstream ringdown family and likelihood-selector certificates inhabit or quote it. The structure itself is pure data; inhabitation is discharged by the concrete witness def that plugs in the Nat/String equalities.
Claim. A certificate is a record asserting: (i) $\mathrm{pyring}+\mathrm{pseobnrv4hm}=N_{\mathrm{H5}}$ and $\mathrm{Kerr}+\mathrm{MMRDNP}+\mathrm{DS}+\mathrm{waveform}=N_{\mathrm{H5}}$; (ii) $N_{\mathrm{H5}}$, total compressed size, and total uncompressed size equal the ZIP-schema totals, with compressed strictly smaller than uncompressed; (iii) the event count is positive; (iv) the smallest and largest members are the named paths $\texttt{rin\_S190727h\_pyring\_DS\_1mode\_10M.h5}$ and $\texttt{rin\_S191109d\_pseobnrv4hm.h5}$; (v) the ZIP schema certificate is inhabited.
background
The module freezes the filename taxonomy of IGWN-GWTC3-TGR-v1-rin.zip from the ZIP central directory alone (Session 118). No posterior samples are opened. Live counts are $N_{\mathrm{H5}}=243$ files over 26 events; pipelines split as pyring $=225$, pseobnrv4hm $=18$; categories as Kerr $=159$, MMRDNP $=44$, damped-sinusoid $=22$, waveform $=18$.
Sibling defs pin those Nat/String constants (taxonomyHDF5FileCount, taxonomyEventCount, taxonomyKerrCount, and so on). The ZIP side comes from the imported ringdown ZIP schema certificate, which supplies ringdownZipH5Count and the compressed/uncompressed byte totals. The present structure is the Prop-bundle that says the taxonomy constants and the ZIP schema agree and that the two natural partitions of the 243 files close.
proof idea
No proof body: this is a structure (definition). Each field is a bare equality, inequality, or Nonempty obligation over the taxonomy constants and the ZIP schema. Inhabitation is supplied downstream by gwtc3RingdownFilenameTaxonomyCert, which fills every field with a named lemma (taxonomy_pipeline_sum, taxonomy_category_sum, taxonomy_hdf5_count_matches_zip_schema, size-match lemmas, the string equalities for smallest/largest member, and the ZIP-schema nonempty witness).
why it matters
This is the structural gate for all GWTC-3 ringdown verification that depends on filename taxonomy rather than on posterior content. The inhabited instance and the one-statement theorem package the same facts for citation. Downstream, the DS 1-mode 10M damping-family certificate requires dsFamilyMemberCount = taxonomyDampedSinusoidCount; the Kerr 2200M family and the likelihood-selector certificate similarly anchor file/model partitions to these counts. Module status is structural theorem: zero sorry, zero new RS axioms, closure dated 2026-05-22. It does not touch the forcing chain (T0–T8) or the mass ladder; it is pure observational bookkeeping that later RS ringdown claims can quote without re-deriving archive layout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.