taxonomy_largest_member_named
plain-language theorem explainer
The largest HDF5 member in the GWTC-3 ringdown ZIP taxonomy is fixed as the path rin/rin_S191109d_pseobnrv4hm.h5. Anyone citing the archive inventory or the master taxonomy certificate uses this identity. The proof is reflexivity against the constant definition.
Claim. The named largest member of the GWTC-3 ringdown filename taxonomy equals the path string $\texttt{rin/rin\_S191109d\_pseobnrv4hm.h5}$.
background
The module records a pure filename taxonomy of the 243 HDF5 files inside IGWN-GWTC3-TGR-v1-rin.zip, taken only from the ZIP central directory. No posterior samples are opened. Live counts include 26 events, pipelines pyring (225) and pseobnrv4hm (18), and categories Kerr, MMRDNP, damped-sinusoid, and waveform.
Among the recorded constants is the largest member path. The definition taxonomyLargestMember is the string literal for that path. Companion counts (HDF5 total, event total, pipeline and category tallies, compressed and uncompressed sizes, and the smallest member) sit beside it as sibling constants. The module status is structural: zero sorry, zero new RS-specific axioms.
proof idea
One-line term proof by rfl. The left-hand side is the definition of the largest-member constant, whose body is exactly the string on the right-hand side, so definitional equality closes the goal.
why it matters
Pins the largest-member field of the archive inventory so the master certificate gwtc3RingdownFilenameTaxonomyCert can package a complete, machine-checkable taxonomy. Downstream the cert bundles pipeline-sum, category-sum, HDF5-count, and compressed-size identities against the ZIP schema. This is verification scaffolding only: it locks the filename census used by reproducibility scripts, not a physics claim about ringdown posteriors or Recognition forcing (T0–T8). It closes one concrete slot in the structural theorem dated 2026-05-22.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.