ringdownZipTopLevelRinCount
plain-language theorem explainer
Records that every entry in the IGWN-GWTC3-TGR-v1-rin.zip central directory carries the top-level prefix rin, with count 244. Cited by the ringdown ZIP schema certificate and the one-statement schema theorem that equate this count to the total entry count. Pure numeric definition, no proof obligation.
Claim. The number of top-level central-directory entries under the prefix $\mathrm{rin}$ in $\texttt{IGWN-GWTC3-TGR-v1-rin.zip}$ is $244$.
background
The module freezes the ZIP central-directory schema of the public IGWN GWTC-3 ringdown archive (IGWN-GWTC3-TGR-v1-rin.zip), obtained by HTTP range request of the central directory alone (about 27 KB), without downloading the 1.44 GB payload. Companion Python script gwtc3_ringdown_zip_schema.py extracts the live metadata.
Among the frozen counts are total entries (244), .h5 files (243), one directory marker, and the top-level prefix tally: every entry sits under rin. This definition is that prefix tally. The module is schema inspection only; it does not touch posterior likelihoods or RS dynamics.
proof idea
Literal Nat definition equal to 244. No tactics, no lemmas. Downstream equality with the total entry count is discharged by unfold and rfl once both constants are unfolded.
why it matters
Pins the structural fact that the archive is a pure rin/ tree (244/244). Feeds ringdown_zip_top_level_count_eq_entries (equality with total entry count), the bundle GWTC3RingdownZipSchemaCert, and the conjunction gwtc3_ringdown_zip_schema_one_statement. Together these close the structural half of the GWTC-3 ringdown verification surface (0 sorry, 0 new RS axioms). No link to the forcing chain T0–T8 or mass ladder; pure external-data hygiene for later TGR comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.