ringdownZipSourceSizeBytes
plain-language theorem explainer
Records the on-disk byte length of the IGWN GWTC-3 ringdown ZIP archive as the natural number 1,444,203,951. Verification authors cite it when checking that the central directory lies strictly inside the file and when assembling the schema certificate. The body is a bare Nat literal, not a derived computation.
Claim. The GWTC-3 ringdown source archive has size $N = 1444203951$ bytes (equivalently $1{,}444{,}203{,}951$).
background
The module freezes structural metadata for IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request of the ZIP central directory only (no full 1.44 GB download). Companion script gwtc3_ringdown_zip_schema.py produced the live numbers: source size, CD offset and size, 244 entries (243 .h5 plus one directory marker), all under the top-level rin prefix, plus aggregate compressed and uncompressed sizes.
This constant is the source-file length in that inventory. Downstream lemmas only need the integer itself; they do not re-fetch the archive. The module is schema inspection, not posterior likelihood, and carries zero sorry and no new RS-specific axioms.
proof idea
Definitional constant: the right-hand side is the Nat literal 1444203951. No tactics, no lemmas. Callers unfold the name and discharge numeric goals with decide.
why it matters
Anchors three local dependents: the positivity fact 0 < source size (used in the schema certificate), the containment inequality that the central-directory interval ends strictly before the end of the file, and the certificate structure GWTC3RingdownZipSchemaCert whose first field is that positivity proof. Together they pin the ZIP layout so later GWTC-3 ringdown verification can treat entry counts and offsets as fixed, audited constants rather than ambient data. No Recognition forcing-chain landmark (T0–T8, RCL, phi) is involved; the declaration is pure experimental-archive bookkeeping inside the Verification domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.