ringdown_zip_entry_count_pos
plain-language theorem explainer
The GWTC-3 ringdown ZIP archive has a strictly positive central-directory entry count (244). Verification and reproducibility authors cite this when assembling the structural schema certificate for IGWN-GWTC3-TGR-v1-rin.zip. The proof unfolds the numeric definition and closes by decidable comparison on naturals.
Claim. The recorded entry count of the GWTC-3 ringdown ZIP central directory is positive: $0 < 244$.
background
The module freezes the ZIP central-directory schema of IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request on the central directory alone (no full 1.44 GB download). Live metadata include source size $1{,}444{,}203{,}951$ bytes, central-directory offset and size, entry count 244, extension tallies (243 .h5, one directory marker), and compressed/uncompressed totals. This is schema inspection only, not posterior likelihood.
The constant ringdownZipEntryCount is the natural number 244, the entry count read from that central directory. Sibling positivity lemmas do the same for source size and central-directory size. The module status is structural theorem: zero sorry, zero new RS-specific axioms.
proof idea
One-line tactic proof: unfold the definition of the entry-count constant (which is the literal natural 244), then decide discharges $0 < 244$ by the decidable order on Nat. No lemmas beyond the definition are required.
why it matters
Feeds the entry_count_pos field of gwtc3RingdownZipSchemaCert, the bundled certificate that the recorded ZIP schema is nonempty and internally consistent (source size positive, CD size positive, entry count positive, extension counts sum to entries, top-level rin prefix count equals entry count). Downstream reproducibility work can point at a machine-checked witness that the ringdown archive is not an empty or degenerate container before any science claim about TGR posteriors is attached. It sits in the Verification domain as infrastructure, not a physics forcing step (T0–T8); it anchors the data side of the GWTC-3 ringdown pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.