gwtc3_ringdown_zip_schema_one_statement
plain-language theorem explainer
Packages the GWTC-3 ringdown ZIP central-directory schema into one conjunction: 244 entries (243 .h5 plus one directory marker), all under the rin prefix, compressed total strictly below uncompressed, manifest key IGWN-GWTC3-TGR-v1-rin.zip, and an inhabited schema certificate. Verification authors cite it when a single closed statement is needed instead of scattered numeric equalities. Term-mode product of rfl on the numeric defs and the component lemmas already proved in-module.
Claim. The GWTC-3 ringdown ZIP has $244$ entries, of which $243$ are $.h5$ files and $1$ is a directory marker; those two counts sum to the entry total; every entry lies under the top-level $\mathrm{rin}$ prefix; total compressed size is strictly less than total uncompressed size; the posterior-manifest key equals $\texttt{IGWN-GWTC3-TGR-v1-rin.zip}$; and the ringdown ZIP schema certificate is inhabited.
background
This module is pure schema inspection of the LIGO/Virgo/KAGRA GWTC-3 ringdown posterior archive IGWN-GWTC3-TGR-v1-rin.zip. Only the ZIP central directory was fetched (about 27 KB at offset ~1.444 GB); the 1.44 GB payload was never downloaded. Companion script gwtc3_ringdown_zip_schema.py produced the live counts that are frozen here as Nat definitions.
Sibling constants record entry count $244$, $.h5$ count $243$, one directory marker, top-level rin prefix count $244$, and the compressed/uncompressed byte totals. The certificate structure GWTC3RingdownZipSchemaCert bundles positivity of source size, central-directory size, and entry count, plus the extension-sum, top-level-equality, and compression inequalities.
Upstream, the posterior manifest fixes ringdownFile.key to the same filename string, proved by ringdown_file_key. The module status line states structural theorem, zero sorry, zero RS-internal axioms.
proof idea
Term-mode eight-component product. The three numeric equalities (entry count $244$, $.h5$ count $243$, directory-marker count $1$) are closed by rfl against the in-module def values. The remaining five conjuncts are the already-proved lemmas ringdown_zip_extension_count_sum, ringdown_zip_top_level_count_eq_entries, ringdown_zip_total_uncompressed_gt_compressed, ringdown_file_key (from the posterior manifest), and gwtc3RingdownZipSchemaCert_inhabited (which wraps the concrete certificate inhabitant). No tactics, no new arithmetic.
why it matters
Closes the structural half of the GWTC-3 ringdown verification surface: once the ZIP schema is a single proved conjunction, downstream reproducibility checks can quote one name rather than re-open eight separate facts. Module doc marks status STRUCTURAL THEOREM with closure date 2026-05-22 and stresses this is schema inspection only, not posterior likelihood. No used_by edges yet; the declaration is a terminal packaging theorem for the ringdown ZIP lane. It does not touch the RS forcing chain (T0–T8), RCL, or mass ladder; it sits in the Verification domain as an external-data integrity lock for GWTC-3 TGR ringdown inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.