taxonomySmallestMember
plain-language theorem explainer
Records the archive path of the smallest HDF5 member in the GWTC-3 ringdown ZIP as a fixed string constant. Anyone citing the Session-118 filename taxonomy or the structural certificate will pull this name. The body is a literal definition, not a derived proof.
Claim. The smallest member of the GWTC-3 ringdown archive taxonomy is the path $\texttt{rin/rin\_S190727h\_pyring\_DS\_1mode\_10M.h5}$.
background
The module freezes the archive-wide filename taxonomy of 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 counts cover events (26), pipelines (pyring 225, pseobnrv4hm 18), and analysis categories (Kerr 159, MMRDNP 44, damped-sinusoid 22, waveform 18).
Among those members the live inventory lists a unique smallest file by compressed size; this definition stores that path as a Lean String. The dual constant for the largest member is recorded beside it. The module is taxonomy only: zero sorry, zero new RS-specific axioms, and no likelihood computation.
proof idea
Pure definitional binding. The right-hand side is the string literal taken from the companion Python taxonomy script and the module inventory; there is no tactic proof or lemma application. Downstream equality is discharged by rfl.
why it matters
Feeds the named reflexivity theorem that pins the smallest-member string, and sits among the numeric constants assembled by the structural certificate GWTC3RingdownFilenameTaxonomyCert (pipeline sum, category sum, HDF5 count matching the ZIP schema). That certificate is the Lean-side closure of the Session-118 ringdown archive inventory. In the broader Verification domain it supplies an auditable, machine-checked label for the lightest ringdown product without touching RS forcing-chain landmarks (T0–T8) or mass-ladder physics; it is pure data hygiene for GWTC-3 reproducibility.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.