ringdownZipCentralDirectorySize
plain-language theorem explainer
Records the ZIP central-directory byte length of IGWN-GWTC3-TGR-v1-rin.zip as the natural number 27558. Verification authors cite it when checking that the directory fits inside the archive and when assembling the schema certificate. It is a bare numeric constant, not a proved statement.
Claim. The central-directory size of the GWTC-3 ringdown ZIP archive is the natural number $27558$ (bytes).
background
The module freezes structural metadata for IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request of the central directory alone (no 1.44 GB payload). Companion measurements include source size $1{,}444{,}203{,}951$ bytes, central-directory offset $1{,}444{,}176{,}371$, entry count $244$, and compressed/uncompressed totals.
This constant is one of several Nat literals that pin the inspected schema. The module is schema inspection only, not posterior likelihood; it carries zero sorry and no new RS-specific axioms. Sibling constants cover source size, offset, entry and extension counts, and aggregate compressed sizes.
proof idea
No proof. The declaration is a definitional abbreviation equal to the literal natural number 27558, matching the live central-directory size reported by the companion Python schema script.
why it matters
Feeds three local consumers: the positivity lemma that $0 < 27558$, the containment theorem that offset plus this size is strictly less than the source archive size, and the certificate structure GWTC3RingdownZipSchemaCert, whose field central_directory_size_pos requires the positivity fact. Together these lock the ZIP layout used for GWTC-3 ringdown verification reproducibility. The module is marked structural theorem with closure 2026-05-22; the constant is the numeric anchor for that closure, not a physics claim about ringdown posteriors or Recognition forcing (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.