ringdown_zip_source_size_pos
plain-language theorem explainer
The recorded byte length of IGWN-GWTC3-TGR-v1-rin.zip is strictly positive. Anyone assembling or citing the GWTC-3 ringdown ZIP schema certificate needs this positivity fact. The proof unfolds the numeric constant and discharges the inequality by decidable arithmetic on naturals.
Claim. The source size of the IGWN-GWTC3-TGR-v1-rin.zip archive, fixed at $1{,}444{,}203{,}951$ bytes, satisfies $0 < 1{,}444{,}203{,}951$.
background
The module freezes the ZIP central-directory schema of IGWN-GWTC3-TGR-v1-rin.zip (GWTC-3 tests of general relativity, ringdown release). Metadata were taken by HTTP range request on the central directory alone, without downloading the full 1.44 GB payload. Companion script: papers/reproducibility/gwtc3_ringdown_zip_schema.py.
Among the frozen fields is the total source size in bytes, defined as the natural number $1{,}444{,}203{,}951$. Related constants record central-directory offset and size, entry count (244), extension tallies (243 .h5 files plus one directory marker), and compressed/uncompressed totals. The module is schema inspection only; it does not touch posterior likelihoods.
Positivity of the source-size constant is a trivial but required well-formedness fact for the schema certificate structure.
proof idea
One-step tactic proof: unfold the definition of the source-size constant (the literal natural $1444203951$), then decide closes $0 < 1444203951$ by the decidable order on Nat. No lemmas beyond that unfolding are required.
why it matters
Feeds the field source_size_pos of gwtc3RingdownZipSchemaCert, the bundled certificate that the frozen ZIP schema is internally consistent (positive sizes, positive entry count, extension counts summing correctly, top-level rin prefix matching entry count). That certificate is the Lean-side anchor for the reproducibility claim that the ringdown archive layout matches the published IGWN release.
In the broader Verification domain this is structural bookkeeping, not a Recognition Science forcing step (T0–T8, RCL, mass ladder). It closes a zero-sorry, zero-new-axiom schema module dated 2026-05-22, so downstream GWTC-3 comparison code can cite a machine-checked size rather than a free-floating magic number.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.