taxonomyPyringCount
plain-language theorem explainer
Records that 225 of the 243 GWTC-3 ringdown HDF5 archive members are pyring-pipeline products, by filename taxonomy only. Anyone auditing the ZIP central-directory census or the pipeline partition cites this constant. It is a literal Nat definition fixed to the Session-118 directory listing, not a derived count.
Claim. In the GWTC-3 ringdown filename taxonomy, the number of archive members attributed to the pyring pipeline is $225$.
background
The module freezes an archive-wide filename taxonomy for the 243 HDF5 files inside IGWN-GWTC3-TGR-v1-rin.zip, using only the ZIP central directory from Session 118. No posterior samples are opened. Companion script: papers/reproducibility/gwtc3_ringdown_filename_taxonomy.py.
Live census in the module doc: 243 HDF5 files, 26 events, pipelines split as pyring $= 225$ and pseobnrv4hm $= 18$, with category split Kerr / MMRDNP / damped-sinusoid / waveform. Sibling constants hold the other census cells (event count, category counts, compressed sizes, extremal members).
This constant is the pyring cell of that pipeline partition. Status is structural: zero sorry, zero new RS-internal axioms; taxonomy only.
proof idea
Definitional constant: the body is the literal natural number 225. No tactic proof, no lemma application. Downstream equalities (pipeline sum, one-statement census) unfold this name and discharge arithmetic by decide.
why it matters
Anchors the pyring side of the pipeline partition used by taxonomy_pipeline_sum (taxonomyPyringCount + taxonomyPSEOBNRv4HMCount = taxonomyHDF5FileCount) and by the certificate structure GWTC3RingdownFilenameTaxonomyCert, whose pipeline_sum field requires that identity. The one-statement theorem gwtc3_ringdown_filename_taxonomy_one_statement packages taxonomyPyringCount = 225 with the rest of the census.
In the Verification domain this is bookkeeping for external GWTC-3 ringdown data hygiene, not a forcing-chain (T0–T8) or RCL step. It closes a reproducibility claim: the Lean census matches the published ZIP directory without reading likelihoods.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.