ringdown_zip_cd_size_pos
plain-language theorem explainer
The GWTC-3 ringdown ZIP central directory has strictly positive byte length (27558). Verification and reproducibility authors cite it when assembling the structural certificate for IGWN-GWTC3-TGR-v1-rin.zip. The proof unfolds the recorded Nat constant and closes by decidable comparison.
Claim. The recorded central-directory size of the GWTC-3 ringdown ZIP archive satisfies $0 < 27558$.
background
This module freezes the ZIP central-directory schema of IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request on the directory only (no full 1.44 GB download). Live metadata include source size $1{,}444{,}203{,}951$ bytes, central-directory offset $1{,}444{,}176{,}371$, central-directory size $27{,}558$ bytes, and $244$ entries.
The constant ringdownZipCentralDirectorySize is the Nat literal $27558$ taken from that inspection. Companion positivity facts cover source size and entry count. The module is schema inspection only, not posterior likelihood; status is structural theorem with zero sorry and no new RS axioms.
proof idea
One-step tactic proof: unfold the definition of the central-directory size constant to the literal $27558$, then decide discharges $0 < 27558$ by native Nat comparison.
why it matters
Feeds the field central_directory_size_pos of gwtc3RingdownZipSchemaCert, the bundled structural certificate for the ringdown ZIP schema. Together with source-size positivity, entry-count positivity, extension-count sum, and top-level prefix equality, it pins that the archived central directory is a non-empty, well-formed object rather than an empty stub. That certificate is the Lean-side anchor for the reproducibility script and the published metadata snapshot; it does not touch RS forcing (T0–T8) or mass ladders, only external data integrity for GWTC-3 ringdown products.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.