ringdown_zip_total_uncompressed_gt_compressed
plain-language theorem explainer
Total compressed entry size of IGWN-GWTC3-TGR-v1-rin.zip is strictly smaller than total uncompressed entry size. Anyone assembling or citing the GWTC-3 ringdown ZIP schema certificate uses this inequality as a basic integrity check on the central-directory totals. The proof unfolds two concrete Nat constants and closes by decidable comparison.
Claim. For the GWTC-3 ringdown archive schema, the summed compressed entry size $1{,}444{,}151{,}741$ is strictly less than the summed uncompressed entry size $1{,}963{,}931{,}876$.
background
The module records the ZIP central-directory schema of IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request on the central directory only (no full 1.44 GB payload). Live metadata include source size $1{,}444{,}203{,}951$ bytes, 244 entries, 243 .h5 files plus one directory marker, and the two size totals used here.
ringdownZipTotalCompressedSize and ringdownZipTotalUncompressedSize are fixed natural-number constants equal to those measured entry-sum totals ($1{,}444{,}151{,}741$ and $1{,}963{,}931{,}876$). The module is schema inspection only, not posterior likelihood; status is structural theorem with zero sorry and no new RS-specific axioms.
proof idea
One-step computational proof. Unfold the two Nat definitions to their literal values, then decide the strict inequality on concrete naturals. No lemmas beyond definitional unfolding are required.
why it matters
Supplies a basic size-integrity fact for the ringdown ZIP schema bundle. Downstream, gwtc3RingdownZipSchemaCert packages positivity and count facts into a single certificate structure, and gwtc3_ringdown_zip_schema_one_statement collapses entry counts, extension split, and top-level rin prefix equality into one conjunction. This inequality is the natural companion check that compressed totals sit strictly below uncompressed totals, matching ordinary ZIP expectations for the GWTC-3 TGR ringdown release. It does not touch the RS forcing chain (T0–T8), RCL, or mass ladder; it is verification scaffolding for external GW catalog data used alongside RS claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.