ringdownZipCentralDirectoryOffset
plain-language theorem explainer
Records the byte offset of the ZIP central directory in IGWN-GWTC3-TGR-v1-rin.zip as the natural number 1,444,176,371. Verification and reproducibility work cites it when checking that the directory lies strictly inside the archive. The body is a bare numeric definition, not a proof.
Claim. Let $N_{\mathrm{cd\_off}} = 1444176371 \in \mathbb{N}$ be the fixed central-directory byte offset of the GWTC-3 ringdown ZIP archive (IGWN-GWTC3-TGR-v1-rin.zip).
background
The module freezes structural metadata for the public GWTC-3 ringdown ZIP (IGWN-GWTC3-TGR-v1-rin.zip), obtained by HTTP range request of the central directory only (no full 1.44 GB download). Companion script: papers/reproducibility/gwtc3_ringdown_zip_schema.py.
Live measured values include source size $1{,}444{,}203{,}951$ bytes, central-directory offset $1{,}444{,}176{,}371$, central-directory size $27{,}558$ bytes, and $244$ entries. This declaration is the Lean binding of that offset. Schema inspection only; it does not encode posterior likelihoods or Recognition Science dynamics.
proof idea
No proof. The declaration is a def equating the name to the literal natural 1444176371, matching the measured central-directory offset from the reproducibility script and module documentation.
why it matters
Feeds the in-bounds check ringdown_zip_cd_inside_source, which asserts offset plus central-directory size is strictly less than the source ZIP size (proved by unfold and decide). Also appears among the numeric anchors of GWTC3RingdownZipSchemaCert, the zero-sorry structural certificate for the ringdown ZIP schema.
In the Verification domain this pins external LIGO/Virgo/KAGRA archive layout so later GWTC-3 comparisons cannot silently drift if the published ZIP is repacked. It is infrastructure for reproducible data hygiene, not a step in the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.