imrFile
plain-language theorem explainer
Names the GWTC-3 inspiral-merger-ringdown (IMR) consistency posterior archive as a typed manifest entry: filename, byte size, and MD5 checksum from Zenodo 7007370. Verification and reproducibility code cite it when assembling the five-file TGR posterior list. The body is a pure structure literal with fixed public metadata.
Claim. Define the IMR consistency posterior-file record with key $\texttt{IGWN-GWTC3-TGR-v1-imr.zip}$, size $4120399443$ bytes, and checksum $\texttt{md5:0a89b6c3d7f43496a4a1b57bb2ac4e32}$.
background
The module freezes the public Zenodo posterior-file manifest for LIGO/Virgo/KAGRA Tests of General Relativity with GWTC-3 (record 7007370). That release supplies five zip archives covering ringdown, inspiral-merger-ringdown consistency, parameterized GR tests, Lorentz-invariance violation, and spin-induced quadrupole moment. Lean records each archive as a PosteriorFile: a triple of filename string, byte length, and checksum string.
This entry is the IMR-consistency archive. The module is posterior-ingestion preparation only: it asserts named files, positive sizes, and a single record id so later ringdown/echo likelihood work can point at real artifacts rather than a status stub. Companion Python fetches the same metadata live from the Zenodo API.
proof idea
No proof. The definition is a structure value of PosteriorFile with three concrete fields: the public zip key, the published byte size, and the MD5 checksum string. Downstream positivity is discharged by decide after unfolding.
why it matters
Feeds the five-element list allPosteriorFiles, the positivity lemma imr_size_pos, the master certificate GWTC3PosteriorManifestCert (field imr_positive), and the one-statement theorem that the manifest names all five TGR zips with positive size. That package upgrades GWTC-3 ringdown status from a placeholder to a pinned posterior artifact path needed for RS echo/QNM likelihood work. It does not itself compute posteriors or test GR; it locks the ingestion contract so verification scripts and Lean certs share one ground truth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.