taxonomyHDF5FileCount
plain-language theorem explainer
Fixes the GWTC-3 ringdown archive size at 243 HDF5 members, taken from the ZIP central directory alone. Downstream taxonomy certificates and the one-statement filename theorem cite this constant as the common total for pipeline and category partitions. The body is a bare natural-number literal; no proof work is required.
Claim. The GWTC-3 ringdown filename taxonomy records exactly $243$ HDF5 files in the archive `IGWN-GWTC3-TGR-v1-rin.zip`.
background
The module is a structural verification layer over LIGO/Virgo/KAGRA GWTC-3 ringdown data. It classifies every member of IGWN-GWTC3-TGR-v1-rin.zip using only the ZIP central directory (Session 118); no posterior samples are opened and no likelihood is evaluated.
Companion constants in the same file fix the rest of the live taxonomy: 26 events; pipelines pyring = 225 and pseobnrv4hm = 18; categories Kerr $159$, MMRDNP $44$, damped-sinusoid $22$, waveform $18$. The imported zip-schema constant ringdownZipH5Count is the independent count of .h5 entries in that archive.
This definition is the single total against which those pipeline and category tallies are checked for partition completeness.
proof idea
Definitional constant: the body is the literal natural number $243$. No tactics, lemmas, or computation are involved. Equality facts that mention it (pipeline sum, category sum, match to the zip schema) discharge by unfold plus decide, or by rfl against the schema constant.
why it matters
Anchors every completeness check in the GWTC-3 ringdown filename taxonomy. The certificate structure GWTC3RingdownFilenameTaxonomyCert requires both pipeline and category sums to equal this total, and requires equality with ringdownZipH5Count. The one-statement theorem packages taxonomyHDF5FileCount = 243 as its first conjunct. The likelihood-selector module reuses the same total so that eligible-plus-blocked file counts match the taxonomy archive size.
Within Recognition Science this is pure external-data hygiene: a zero-sorry, zero-new-axiom lock on the observational corpus before any RS mass or ringdown claim is attached. It does not itself invoke the forcing chain (T0–T8), the Recognition Composition Law, or the phi-ladder; it only certifies that the file set under study is fully accounted for.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.