ringdownZipH5Count
plain-language theorem explainer
Records that the GWTC-3 ringdown ZIP contains exactly 243 HDF5 entries. Verification authors cite it when locking the archive layout against filename taxonomies and certificate structures. The body is a bare natural-number literal fixed by central-directory inspection of IGWN-GWTC3-TGR-v1-rin.zip.
Claim. The number of $.h5$ entries in the IGWN-GWTC3 ringdown ZIP central directory is $243$.
background
The module freezes the ZIP central-directory schema of IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request on the directory alone (no full 1.44 GB download). Live metadata give source size $1{,}444{,}203{,}951$ bytes, $244$ total entries, extension split $.h5 = 243$ and bare directory marker $= 1$, and top-level prefix rin on every entry.
This constant is the HDF5 half of that extension split. Companion definitions fix entry count, directory-marker count, byte sizes, and compressed/uncompressed totals. The setting is pure schema inspection: file names and sizes only, not posterior likelihoods or TGR model content. Zero sorry and no new RS-specific axioms.
proof idea
Definitional constant: the natural number $243$ is written literally. Downstream equalities such as the extension-count sum unfold the three constants and discharge by decide; the taxonomy match is rfl against the parallel HDF5 file-count literal.
why it matters
Feeds the ringdown ZIP schema certificate (extension-count sum equating HDF5 count plus directory marker to total entries) and the one-statement schema theorem that packages entry count $244$, HDF5 count $243$, marker count $1$, and the rin prefix identity. Also anchors the filename-taxonomy certificate via taxonomyHDF5FileCount = ringdownZipH5Count, so pipeline and category partitions are forced to the same archive layout. Closes a reproducibility pin for GWTC-3 ringdown data used in external verification; it is structural bookkeeping, not a physics derivation from the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.