ringdownZipDirectoryMarkerCount
plain-language theorem explainer
Records that the GWTC-3 ringdown ZIP central directory contains exactly one directory-marker entry (no file extension). Verification authors cite it when checking that HDF5 files plus this marker exhaust the entry list. It is a literal natural-number constant fixed by the inspected schema, not a derived proof.
Claim. The number of directory-marker entries (central-directory records with no file extension) in the IGWN-GWTC3-TGR-v1 ringdown ZIP is $1$.
background
The module freezes structural metadata of IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request on the ZIP central directory only (no full 1.44 GB download). Companion measurements list 244 entries: 243 .h5 files and one extensionless directory marker, all under the top-level rin prefix.
This constant is one of several schema literals (source size, central-directory offset and size, entry and extension counts, compressed and uncompressed totals). The module is schema inspection only; it does not encode posterior likelihoods or Recognition Science dynamics.
Sibling counts include the HDF5 entry total and the overall entry total. Their arithmetic relation is the local consistency check that the marker count participates in.
proof idea
No proof body: a definition that binds a natural number to the literal value 1, matching the live central-directory scan (one extensionless directory marker). Downstream lemmas unfold this binder and discharge equalities by decide.
why it matters
Feeds three local consumers: the certificate structure requires that the HDF5 count plus this marker count equals the entry count; the one-statement schema theorem asserts the marker count equals 1 as a conjunct; and the extension-count-sum theorem proves that addition identity by unfolding the three constants.
In the broader Verification domain this is structural closure for the GWTC-3 ringdown archive layout (status: structural theorem, zero sorry, zero new RS axioms). It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it only pins reproducible archive geometry so later posterior or TGR checks can name a fixed file inventory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.