gwtc3RingdownZipSchemaCert
plain-language theorem explainer
Packages the inspected ZIP central-directory facts for IGWN-GWTC3-TGR-v1-rin.zip into one inhabited certificate: positive sizes and entry count, extension and top-level counts that sum to the entry total, uncompressed larger than compressed, and the central directory lying inside the archive, with the manifest key fixed. Verification authors cite it when they need a single witness that the ringdown archive schema is well-formed. The body is a pure structure instance wiring seven decide-proved lemmas plus the manifest key theorem.
Claim. There is a certificate recording that the GWTC-3 ringdown ZIP has positive source size and positive central-directory size, positive entry count, $.h5$ count plus directory-marker count equal to the entry count, top-level $rin$ count equal to the entry count, total compressed size strictly less than total uncompressed size, central-directory offset plus size strictly inside the source length, and that the ringdown manifest key is exactly $\texttt{IGWN-GWTC3-TGR-v1-rin.zip}$.
background
The module is a structural audit of IGWN-GWTC3-TGR-v1-rin.zip (GWTC-3 ringdown release). Only the ZIP central directory was fetched by HTTP range request; the ~1.44 GB payload is never loaded. Live metadata fixed in the module: source size $1{,}444{,}203{,}951$ bytes, central-directory offset $1{,}444{,}176{,}371$, size $27{,}558$ bytes, $244$ entries ($243$ .h5, one directory marker), all under the top-level rin prefix, with total compressed $1{,}444{,}151{,}741$ and uncompressed $1{,}963{,}931{,}876$ bytes.
GWTC3RingdownZipSchemaCert is the structure that bundles the positivity, counting, and containment inequalities on those constants. Upstream lemmas such as ringdown_zip_source_size_pos, ringdown_zip_cd_size_pos, ringdown_zip_entry_count_pos, ringdown_zip_extension_count_sum, and ringdown_zip_cd_inside_source discharge each field by unfolding the numeric defs and decide. The companion theorem ringdown_file_key pins the manifest name to the same archive string. This is schema inspection only, not posterior likelihood.
proof idea
Definitional structure instance, not a tactic proof. Each field of GWTC3RingdownZipSchemaCert is filled by the corresponding upstream lemma: positivity of source size, central-directory size, and entry count; the extension-count sum; top-level count equality; uncompressed strictly above compressed; central directory strictly inside the source; and the manifest key theorem ringdown_file_key (proved by rfl). Those lemmas themselves are one-line unfold ...; decide reductions on the frozen numeric constants. No new reasoning appears here beyond wiring the witnesses.
why it matters
Gives a single inhabited certificate that the ringdown ZIP schema is internally consistent, which the sibling theorem gwtc3RingdownZipSchemaCert_inhabited exposes as Nonempty GWTC3RingdownZipSchemaCert. Downstream verification can therefore assume the archive layout (positive sizes, 244 entries under rin, CD inside bounds, correct manifest key) without re-proving each numeric fact. In the Recognition verification stack this closes the structural side of the GWTC-3 ringdown data path (module status: 0 sorry, 0 RS-internal axioms). It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it is pure observational hygiene for gravitational-wave posterior inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.