taxonomy_uncompressed_gt_compressed
plain-language theorem explainer
The GWTC-3 ringdown ZIP archive has strictly smaller total compressed size than total uncompressed size: 1,444,151,741 < 1,963,931,876 bytes. Archive and reproducibility auditors cite this as a sanity check that the Session-118 central-directory totals are ordered as a real ZIP must be. The proof unfolds the two Nat constants and closes by decidable comparison.
Claim. The archive-wide total compressed size of the GWTC-3 ringdown taxonomy is strictly less than the total uncompressed size: $1444151741 < 1963931876$.
background
This module is a structural taxonomy of the 243 HDF5 members in IGWN-GWTC3-TGR-v1-rin.zip, built only from the ZIP central directory (Session 118). No posterior samples are read. Live counts include 26 events, pipelines pyring (225) and pseobnrv4hm (18), and categories Kerr, MMRDNP, damped-sinusoid, and waveform.
Two Nat constants record the archive-wide byte totals extracted from that directory: total compressed size $1444151741$ and total uncompressed size $1963931876$. They sit beside sibling counts (HDF5 file count, event count, pipeline and category tallies, smallest and largest members). The module status is structural theorem: zero sorry, zero new RS-internal axioms.
proof idea
One-line tactic proof. Unfold the two definitions to the concrete natural numbers $1444151741$ and $1963931876$, then close the strict inequality by decide on Nat comparison. No lemmas beyond definitional unfolding are required.
why it matters
Feeds the bundle certificate gwtc3RingdownFilenameTaxonomyCert, which packages pipeline and category sum identities, HDF5 count agreement with the ZIP schema, and compressed-size agreement with the schema. The inequality is a cheap integrity check that the recorded compressed and uncompressed totals are ordered as a genuine ZIP central directory must be, before those totals are equated to the schema side.
Within Recognition Science verification, this is archive hygiene rather than a forcing-chain step (T0–T8). It locks the filename taxonomy layer so downstream GWTC-3 ringdown claims cannot silently drift from the Session-118 directory snapshot. Companion script: papers/reproducibility/gwtc3_ringdown_filename_taxonomy.py.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.