taxonomy_event_count_pos
plain-language theorem explainer
The GWTC-3 ringdown filename taxonomy records a strictly positive number of distinct events. Anyone citing the archive-wide count of 26 events in IGWN-GWTC3-TGR-v1-rin.zip needs this positivity fact. The proof unfolds the constant definition and discharges the inequality by decision procedure.
Claim. The number of distinct events catalogued in the GWTC-3 ringdown filename taxonomy is strictly positive: $0 < 26$.
background
The module is a structural record of the archive-wide filename taxonomy of the 243 HDF5 files inside IGWN-GWTC3-TGR-v1-rin.zip. It uses only the ZIP central directory; no posterior samples are read. Live counts include 26 events, pipelines pyring (225) and pseobnrv4hm (18), and categories Kerr, MMRDNP, damped-sinusoid, and waveform.
The event count is the bare natural-number constant 26. Sibling constants fix HDF5 file totals, pipeline and category tallies, compressed and uncompressed sizes, and extremal members. The module status is structural theorem: zero sorry, zero RS-internal axioms.
proof idea
One-line term-style proof: unfold the definition of the event-count constant (which is literally 26), then decide closes $0 < 26$ by the decidable order on naturals. No lemmas beyond the definition are required.
why it matters
The positivity fact is a field obligation inside the aggregate certificate gwtc3RingdownFilenameTaxonomyCert, which packages pipeline-sum, category-sum, HDF5-count, and compressed-size matches against the ZIP schema. It guarantees the taxonomy is non-vacuous before those equalities are asserted. The module is verification scaffolding only: taxonomy of filenames, not a physics claim about ringdown posteriors or Recognition Science forcing (T0–T8). It closes a reproducibility checkpoint for the companion Python taxonomy script.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.