ringdownZipEntryCount
plain-language theorem explainer
The GWTC-3 ringdown ZIP central directory contains exactly 244 entries. Verification and reproducibility work cites this constant when locking the IGWN-GWTC3-TGR-v1-rin.zip layout without downloading the 1.44 GB payload. It is a bare natural-number definition fixed by live HTTP range inspection of the archive.
Claim. The number of entries in the central directory of the GWTC-3 ringdown ZIP archive $\mathrm{IGWN\text{-}GWTC3\text{-}TGR\text{-}v1\text{-}rin.zip}$ is the natural number $244$.
background
The module records structural metadata of the public LIGO/Virgo/KAGRA GWTC-3 tests-of-general-relativity ringdown release archive. Only the ZIP central directory is fetched by HTTP range request; the full 1.44 GB payload is never downloaded. Companion Python under papers/reproducibility/ performs the live inspection.
Live metadata include source size $1{,}444{,}203{,}951$ bytes, central-directory offset and size, entry count $244$, extension split $.h5 = 243$ plus one directory marker, uniform top-level prefix rin, and aggregate compressed/uncompressed sizes. The module is schema inspection only, not posterior likelihood, and carries zero sorry and no new RS-specific axioms.
Sibling constants fix the other measured fields (source size, CD offset/size, H5 and directory-marker counts, top-level rin count, total compressed and uncompressed sizes). Positivity and partition lemmas are proved from those constants by unfold and decide/rfl.
proof idea
No proof body: the declaration is a definition equating the entry-count constant to the literal natural number 244. Downstream positivity and partition facts simply unfold this definition and discharge the resulting numeral goals by decide or rfl.
why it matters
The constant is the numeric anchor for the ringdown ZIP schema certificate structure, which requires positivity of the entry count and the partition identity that H5 count plus directory-marker count equals total entries. It appears in the one-statement schema theorem that packages entry count, extension counts, their sum, top-level rin equality, and related size facts into a single conjunction.
Direct consumers include the positivity lemma for the entry count, the extension-count sum lemma, and the top-level count equality. Together they close the structural half of the GWTC-3 ringdown verification path: the archive layout is pinned in Lean so later scientific claims can cite a machine-checked schema rather than an external file listing. This is verification scaffolding for external GW data, not a step of the T0–T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.