allPosteriorFiles
plain-language theorem explainer
The complete ordered list of five GWTC-3 tests-of-GR posterior zip files from Zenodo record 7007370 (IMR consistency, ringdown, spin-induced quadrupole, Lorentz violation, parameterized GR). Anyone citing the posterior-manifest completeness or positivity theorems uses this list as the single source of file entries. It is a plain list literal of the five named PosteriorFile records.
Claim. Define the GWTC-3 posterior-file manifest as the list of five entries: the IMR-consistency zip, the ringdown zip, the spin-induced-quadrupole zip, the Lorentz-invariance-violation zip, and the parameterized-GR zip, each carrying its Zenodo key, byte size, and MD5 checksum.
background
This module is posterior-ingestion preparation for upgrading GWTC-3 ringdown status into a real likelihood artifact. It pins the public Zenodo release "Data release for Tests of General Relativity with GWTC-3" (record id 7007370) and the five required zip archives that hold the TGR posterior samples.
A PosteriorFile is a triple: string key (filename), natural-number size in bytes, and checksum string. The five sibling constants fix the concrete Zenodo names and sizes: IMR consistency (~4.1 GB), ringdown (IGWN-GWTC3-TGR-v1-rin.zip), spin-induced quadrupole, Lorentz-invariance violation (~7.4 GB), and parameterized GR tests.
The Lean content is structural only: name the files, assert positive sizes, and tie them to one record id. A companion Python script re-fetches the same metadata live from the Zenodo API. This is not a likelihood computation and introduces no RS-internal axioms.
proof idea
Definition by list literal. The body is the five-element list of the already-defined file records (IMR, ringdown, SIM, LIV, parameterized GR) in that fixed order. No tactics, no lemmas, no computation beyond constructing the list.
why it matters
This list is the single source of truth for manifest completeness. Downstream, posterior_manifest_has_five_files unfolds it and decides that its length equals 5; GWTC3PosteriorManifestCert packages that length fact with positivity of each file and a positive Zenodo record id; and gwtc3_posterior_manifest_one_statement conjoins record id, length five, the explicit ringdown key, and all five positivity witnesses into one citation theorem.
In the broader Recognition verification layer this closes the structural prerequisite for ringdown/echo QNM posterior work against GWTC-3: the ringdown zip is named and sized before any likelihood is attached. It does not itself touch the forcing chain (T0–T8), RCL, or mass ladder; it is pure observational-data bookkeeping that keeps the GR-test posteriors machine-checkably identified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.