ringdown_zip_top_level_count_eq_entries
plain-language theorem explainer
The top-level `rin` prefix count equals the total entry count in the GWTC-3 ringdown ZIP central directory (both fixed at 244). Schema-certificate and one-statement packaging theorems cite this equality. The proof unfolds the two Nat constants and closes by reflexivity.
Claim. In the recorded central-directory schema of the GWTC-3 ringdown archive, the number of top-level entries under the prefix $\mathrm{rin}$ equals the total number of ZIP entries: both are $244$.
background
This module freezes structural metadata of IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request of the central directory only (no full 1.44 GB payload). Live inspection reports source size $1{,}444{,}203{,}951$ bytes, central-directory size $27{,}558$ bytes, and $244$ entries, of which $243$ are .h5 files and one is a directory marker; every entry sits under the top-level prefix rin.
Two sibling constants encode those counts: ringdownZipEntryCount := 244 and ringdownZipTopLevelRinCount := 244. The module is schema inspection only, not posterior likelihood, and carries zero sorry and no new RS-specific axioms.
proof idea
One-line tactic proof: unfold both Nat definitions, then close by rfl. No lemmas are needed; the equality is definitional once the constants are expanded to the shared literal $244$.
why it matters
The equality is a field of gwtc3RingdownZipSchemaCert, the bundled certificate structure for the ringdown ZIP schema. It also appears as one conjunct in gwtc3_ringdown_zip_schema_one_statement, the single-statement packaging theorem that asserts entry count, extension split, and top-level prefix agreement together.
In the Recognition verification layer this is pure archival hygiene: it locks the claim that every central-directory entry is a top-level rin path, so downstream consumers cannot silently drop or rename files when replaying the GWTC-3 ringdown schema. It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it only certifies external data layout used by later empirical checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.