ringdown_size_pos
plain-language theorem explainer
The GWTC-3 ringdown posterior zip is recorded with a strictly positive byte size in the Zenodo manifest. Anyone assembling the GWTC-3 posterior-manifest certificate or the one-statement completeness theorem cites this fact. The proof unfolds the positivity predicate and the file record, then closes by decidable Nat comparison.
Claim. The ringdown posterior-file entry with key $\mathrm{IGWN\text{-}GWTC3\text{-}TGR\text{-}v1\text{-}rin.zip}$ and recorded size $1444203951$ bytes satisfies $0 < \mathrm{sizeBytes}$.
background
This module is structural verification infrastructure: it freezes the public Zenodo record 7007370 ("Data release for Tests of General Relativity with GWTC-3") as a Lean manifest of five posterior zip files. It is posterior-ingestion preparation, not a likelihood evaluation.
A PosteriorFile is a triple of string key, natural-number byte size, and checksum string. Positivity is the predicate $0 < f.\mathrm{sizeBytes}$. The ringdown entry is the concrete record with key IGWN-GWTC3-TGR-v1-rin.zip, size $1444203951$, and the listed MD5 checksum; that is the file the module flags as required for ringdown / QNM posterior work.
proof idea
One-line tactic proof. Unfold the positivity predicate and the ringdown file definition so the goal is the concrete inequality $0 < 1444203951$ on Nat, then close with decide. No lemmas beyond definitional unfolding.
why it matters
Feeds the certificate bundle gwtc3PosteriorManifestCert as the ringdown_positive field, and appears as one conjunct in gwtc3_posterior_manifest_one_statement, whose doc-comment states the manifest "names all five expected tests-of-GR zip files, including the ringdown file required for RS echo/QNM posterior likelihood work."
In the Recognition pipeline this is the structural gate before any RS ringdown-status upgrade: without a named, positive-size ringdown artifact pinned to Zenodo 7007370, later echo/QNM posterior claims have no fixed public data handle. Zero sorry; no RS-internal axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.