ringdownZipTotalUncompressedSize
plain-language theorem explainer
Records the total uncompressed byte size of all entries in the IGWN-GWTC3-TGR-v1-rin.zip central directory as the natural number 1,963,931,876. Verification authors cite it when matching filename-taxonomy aggregates to the live ZIP schema and when proving compressed size is strictly smaller. It is a bare Nat literal pinned by the companion HTTP-range schema script.
Claim. The total uncompressed size of entries in the GWTC-3 ringdown ZIP archive is the natural number $1{,}963{,}931{,}876$ (bytes).
background
The module freezes the ZIP central-directory schema of IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request of the central directory only (no full 1.44 GB download). Companion script papers/reproducibility/gwtc3_ringdown_zip_schema.py reports live metadata: source size 1,444,203,951 bytes, 244 entries, 243 .h5 files plus one directory marker, all under the top-level rin prefix.
Among those metadata constants, the sum of per-entry uncompressed sizes is listed as 1,963,931,876 bytes. Sibling definitions pin source size, central-directory offset and size, entry counts, and total compressed size (1,444,151,741). The module is schema inspection only, not posterior likelihood; status is structural with zero sorry and no new RS axioms.
proof idea
Definitional constant: a single Nat literal 1963931876. No tactics, no lemmas. Downstream inequalities and equalities unfold this name and discharge by rfl or decide.
why it matters
Feeds the ringdown ZIP schema certificate and the one-statement schema theorem, which package entry counts, extension sums, and size positivity. The strict inequality ringdown_zip_total_uncompressed_gt_compressed unfolds this constant against the compressed total and closes by decide. Filename taxonomy uses it in taxonomy_total_uncompressed_matches_zip_schema (taxonomyTotalUncompressedSize = ringdownZipTotalUncompressedSize by rfl) and in the taxonomy certificate that aligns HDF5 counts with the ZIP schema. Together these lock the external GWTC-3 ringdown archive layout into the verification layer so later RS claims about ringdown posteriors rest on a fixed, reproducible byte budget rather than a floating download.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.