ringdown_zip_cd_inside_source
plain-language theorem explainer
The GWTC-3 ringdown ZIP central directory lies strictly inside the archive: offset plus size is less than the source byte length. Anyone assembling or citing the ringdown ZIP schema certificate needs this bound. The proof unfolds three Nat constants and closes by decidable arithmetic.
Claim. For the IGWN-GWTC3-TGR-v1-rin.zip archive, the central-directory offset plus its byte length is strictly less than the source size: $1{,}444{,}176{,}371 + 27{,}558 < 1{,}444{,}203{,}951$.
background
This module freezes the ZIP central-directory schema of IGWN-GWTC3-TGR-v1-rin.zip, obtained by HTTP range request of the directory only (no full 1.44 GB download). It is schema inspection, not posterior likelihood. Live metadata include source size $1{,}444{,}203{,}951$ bytes, central-directory offset $1{,}444{,}176{,}371$, and central-directory size $27{,}558$ bytes.
The three quantities are module-level Nat definitions: ringdownZipSourceSizeBytes, ringdownZipCentralDirectoryOffset, and ringdownZipCentralDirectorySize. A well-formed ZIP requires the central directory to sit entirely inside the file, which is exactly the strict inequality proved here. Companion positivity lemmas (source size, CD size, entry count) live in the same file.
proof idea
Term-mode proof by unfolding the three Nat definitions to their concrete values, then decide on the closed arithmetic inequality $1444176371 + 27558 < 1444203951$. No lemmas beyond the definitions themselves.
why it matters
Feeds the master certificate gwtc3RingdownZipSchemaCert, which packages the structural facts about the ringdown ZIP (positive sizes, entry counts, extension tallies, top-level prefix). Without the CD-inside-source bound, the schema could describe a directory that overruns the archive, so the certificate would not certify a coherent ZIP layout.
In the Recognition verification layer this is pure external-data hygiene: it locks the GWTC-3 ringdown archive geometry used by downstream TGR checks. It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it only guarantees that the cited observational ZIP is internally consistent at the byte-layout level. Status is fully proved (0 sorry, 0 new RS axioms).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.