taxonomyTotalCompressedSize
plain-language theorem explainer
Fixes the total compressed byte count of the GWTC-3 ringdown ZIP archive at 1 444 151 741. Verification authors cite it when checking that the filename taxonomy agrees with the Session-118 ZIP central directory. It is a bare natural-number constant, not a derived claim.
Claim. The total compressed size of the GWTC-3 ringdown archive (all 243 HDF5 members in `IGWN-GWTC3-TGR-v1-rin.zip`) is the natural number $1444151741$.
background
The module freezes an archive-wide filename taxonomy for the 243 HDF5 files inside IGWN-GWTC3-TGR-v1-rin.zip. Only the ZIP central directory from Session 118 is used; no posterior samples are opened. Companion counts cover events (26), pipelines (pyring 225, pseobnrv4hm 18), and analysis categories (Kerr, MMRDNP, damped-sinusoid, waveform).
Sibling constants record the matching uncompressed total, the smallest and largest members, and the per-pipeline and per-category tallies. The imported ZIP schema supplies the independent compressed-size figure that this constant is later compared against. Status is structural: zero sorry, zero new RS axioms.
proof idea
Literal definition: the natural number 1444151741 is assigned directly. No lemmas, tactics, or computation appear in the body.
why it matters
Anchors three local checks. The theorem taxonomy_total_compressed_matches_zip_schema asserts definitional equality with the ZIP-schema total compressed size (proved by rfl). The inequality taxonomy_uncompressed_gt_compressed uses both size constants and closes by decide. The certificate structure GWTC3RingdownFilenameTaxonomyCert packages the taxonomy invariants (pipeline and category sums, HDF5 count match) that sit beside these size facts.
In the broader Verification domain this is pure archival bookkeeping: it lets later RS claims about ringdown data cite a machine-checked inventory without re-parsing the ZIP. It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it only certifies that the external GWTC-3 ringdown corpus is the one the reproducibility scripts claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.