GWTC3RingdownZipSchemaCert
plain-language theorem explainer
Certificate structure packaging the measured ZIP central-directory invariants of the GWTC-3 ringdown archive (IGWN-GWTC3-TGR-v1-rin.zip): positive sizes and entry counts, extension and top-level prefix accounting, compression inequality, and central-directory containment. Downstream taxonomy and HDF5 sample certificates cite it as the schema spine. No proof body: the structure is the claim bundle; a concrete inhabitant discharges every field by Nat arithmetic on fixed constants.
Claim. A certificate asserting: source ZIP size $>0$; central-directory size $>0$; entry count $>0$; $(\#\text{.h5})+(\#\text{directory markers})=\text{entry count}$; top-level $\texttt{rin}$ prefix count equals entry count; total compressed size $<$ total uncompressed size; central-directory offset plus size is strictly inside the source; and the posterior-manifest key equals $\texttt{IGWN-GWTC3-TGR-v1-rin.zip}$.
background
The module records the ZIP central-directory schema of the LIGO/Virgo/KAGRA GWTC-3 ringdown release archive, obtained by HTTP range request of the central directory only (no full 1.44 GB download). Companion script gwtc3_ringdown_zip_schema.py produced the live metadata: source size $1{,}444{,}203{,}951$ B, CD offset $1{,}444{,}176{,}371$, CD size $27{,}558$ B, $244$ entries ($243$ .h5, one directory marker), all under top-level prefix rin, with total compressed $1{,}444{,}151{,}741$ B and uncompressed $1{,}963{,}931{,}876$ B.
Sibling defs freeze those measurements as Nat constants (ringdownZipEntryCount := 244, ringdownZipH5Count, ringdownZipCentralDirectoryOffset, etc.). The posterior manifest supplies ringdownFile with the same filename key and size. This is pure schema inspection, not posterior likelihood. Status: structural, zero sorry, zero new RS axioms.
proof idea
Definitional structure: eight fields, each a Prop over the frozen Nat constants and the manifest key. No tactic proof lives on the structure itself. The concrete value gwtc3RingdownZipSchemaCert fills every field by naming the corresponding positivity or equality lemmas (ringdown_zip_source_size_pos, ringdown_zip_cd_size_pos, ringdown_zip_entry_count_pos, extension-count and top-level equalities, and the remaining arithmetic facts). Nonempty follows by packing that inhabitant. The one-statement theorem then projects the numeric equalities as a single conjunction.
why it matters
Anchors the GWTC-3 ringdown verification stack. Filename taxonomy certificates require taxonomyHDF5FileCount = ringdownZipH5Count and therefore inherit the ZIP entry accounting. HDF5 sample-schema certificates sit on the same archive and reuse the compression and naming conventions. The module's own gwtc3_ringdown_zip_schema_one_statement collapses the certificate into a single conjunction of the measured counts. In the broader Recognition verification layer this is empirical infrastructure: it pins the external GWTC-3 ringdown data product so later RS claims about ringdown posteriors cannot silently drift from the published archive layout. Not a forcing-chain (T0–T8) step; it is data-schema closure for observational cross-checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.