ringdown_zip_extension_count_sum
plain-language theorem explainer
The GWTC-3 ringdown ZIP has 243 HDF5 entries and one extensionless directory marker, and those counts sum to the total entry count 244. Schema-verification authors cite this when assembling the central-directory certificate. The proof unfolds three literal Nat constants and closes by decidable arithmetic.
Claim. In the GWTC-3 ringdown ZIP central directory, the number of $.h5$ entries plus the number of extensionless directory markers equals the total entry count: $243 + 1 = 244$.
background
The module freezes the ZIP central-directory schema of IGWN-GWTC3-TGR-v1-rin.zip, fetched by HTTP range request on the central directory alone (no full 1.44 GB download). Live metadata lists source size $1{,}444{,}203{,}951$ bytes, central-directory size $27{,}558$ bytes, and $244$ entries under the top-level rin prefix.
Three Nat constants record the extension split: total entries $244$, $.h5$ files $243$, and one extensionless directory marker. The module is schema inspection only, not posterior likelihood; it carries zero sorry and no new RS-specific axioms.
proof idea
Tactic proof in two steps: unfold the three Nat definitions to the literals $243$, $1$, and $244$, then decide discharges $243 + 1 = 244$ by computation. No lemmas beyond the definitions themselves.
why it matters
Supplies the extension_count_sum field of the certificate record that bundles all positive-size and count identities for the ringdown ZIP. It also appears as an explicit conjunct in the one-statement schema theorem, which packages entry count, extension split, and top-level prefix equality into a single Prop. Downstream consumers use that certificate as the structural gate before any science-level use of the GWTC-3 ringdown archive. This is observational schema hygiene, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.