taxonomyLargestMember
plain-language theorem explainer
Records the ZIP path of the single largest HDF5 member in the GWTC-3 ringdown archive: rin/rin_S191109d_pseobnrv4hm.h5. Anyone auditing the filename taxonomy or the master cert cites this constant. The body is a bare string literal, not a derived computation.
Claim. The largest member (by compressed size in the ZIP central directory) among the $243$ GWTC-3 ringdown HDF5 files is the archive path $\texttt{rin/rin\_S191109d\_pseobnrv4hm.h5}$.
background
The module freezes an archive-wide filename taxonomy of the $243$ HDF5 files inside IGWN-GWTC3-TGR-v1-rin.zip, using only the ZIP central directory. No posterior samples are opened. Companion counts fix $26$ events, pipelines pyring = 225 and pseobnrv4hm = 18, and categories Kerr $159$, MMRDNP $44$, damped-sinusoid $22$, waveform $18$.
Sibling constants pin the extremes: the smallest member is rin/rin_S190727h_pyring_DS_1mode_10M.h5; this definition pins the largest. Both come from the external reproducibility script and are reified as Lean strings so downstream equalities can be rfl.
proof idea
Definitional constant: the right-hand side is the string literal "rin/rin_S191109d_pseobnrv4hm.h5". No lemma, tactic, or computation runs in Lean; the value is the frozen taxonomy fact from the ZIP listing.
why it matters
Feeds two local consumers. The theorem taxonomy_largest_member_named is the reflexivity witness that this constant equals the documented path. The master structure GWTC3RingdownFilenameTaxonomyCert packages pipeline and category sum identities together with the HDF5 count match against the ZIP schema; the largest-member name is part of the same frozen taxonomy surface those identities sit on.
In the broader Verification domain this is structural bookkeeping only: it locks the archive inventory so later RS claims about ringdown data cannot silently drift from the published GWTC-3 TGR release. It does not touch forcing-chain landmarks (T5–T8), RCL, or mass-ladder physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.