ringdownZipTotalCompressedSize
plain-language theorem explainer
Records the summed compressed byte size of every entry in IGWN-GWTC3-TGR-v1-rin.zip as the natural number 1,444,151,741. Verification and taxonomy modules cite it when matching filename-level compressed totals to the ZIP central directory and when proving uncompressed size strictly exceeds compressed size. The body is a bare Nat literal fixed by the companion schema script.
Claim. The total compressed size of all central-directory entries in the GWTC-3 ringdown ZIP archive equals $1{,}444{,}151{,}741$ bytes.
background
The module freezes structural metadata of IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request of the ZIP central directory alone (no full 1.44 GB payload). Companion script gwtc3_ringdown_zip_schema.py reports source size, central-directory offset and size, entry counts by extension, and the two aggregate sizes: total compressed and total uncompressed.
This constant is the compressed aggregate: sum of compressed sizes listed for the 244 entries (243 .h5 files plus one directory marker). It is schema inspection only, not a posterior or likelihood claim. Sibling constants fix source size, CD offset/size, entry counts, and the matching uncompressed total $1{,}963{,}931{,}876$.
proof idea
Definitional constant: the body is the Nat literal 1444151741, transcribed from the live central-directory scan. No proof obligations, tactics, or upstream lemmas.
why it matters
Anchors several verification certificates. taxonomy_total_compressed_matches_zip_schema equates the filename-taxonomy compressed total to this value by rfl. ringdown_zip_total_uncompressed_gt_compressed unfolds this constant against the uncompressed total and closes by decide. The one-statement schema theorem and GWTC3RingdownZipSchemaCert / GWTC3RingdownFilenameTaxonomyCert structures thread the same figure so that ZIP-level and taxonomy-level bookkeeping stay definitionally aligned.
In the broader Recognition verification layer this is pure external-data hygiene: a frozen, machine-checkable snapshot of public GWTC-3 ringdown packaging, with zero sorry and no RS-internal axioms. It does not touch the forcing chain (T0–T8), J-cost, or mass ladder; it only certifies that the ringdown archive used downstream is the one whose compressed footprint is this number.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.