ringdownFile
plain-language theorem explainer
Names the GWTC-3 ringdown posterior zip as a concrete manifest entry: filename IGWN-GWTC3-TGR-v1-rin.zip, size 1 444 203 951 bytes, MD5 131d4d5e057f5e1c58787ca2920796a4. Anyone wiring LIGO/Virgo tests-of-GR posteriors into RS echo or QNM likelihood work cites this entry. It is a pure structure instance, not a proved statement.
Claim. The ringdown posterior-file entry is the triple $(\texttt{IGWN-GWTC3-TGR-v1-rin.zip},\, 1444203951,\, \texttt{md5:131d4d5e057f5e1c58787ca2920796a4})$ in the GWTC-3 Zenodo posterior manifest (record $7007370$).
background
Module GWTC3PosteriorManifest freezes the public Zenodo data release for Tests of General Relativity with GWTC-3 (record 7007370). It is posterior-ingestion preparation: five expected zip files are named, sized, and checksummed so later certificates can treat the catalog as a fixed artifact rather than a status flag.
A posterior-file entry is a triple of filename key, byte size, and checksum string. The five required archives cover ringdown, inspiral-merger-ringdown consistency, parameterized GR tests, Lorentz-invariance violation, and spin-induced quadrupole moment. The companion Python script re-fetches the same metadata live from the Zenodo API.
This entry is the ringdown archive specifically. Downstream RS work on echoes and quasinormal-mode posteriors needs that file named and size-positive before any likelihood is attached.
proof idea
Definitional structure instance. The three fields of PosteriorFile are filled by string and natural literals: key, sizeBytes, and checksum. No tactics, no lemmas, no computation beyond the literal assignment.
why it matters
Anchors the ringdown half of the GWTC-3 posterior manifest. It is listed in the five-file roster, supplies the key equality and positive-size facts used by the master one-statement theorem, and is required by the ringdown-zip schema certificate (source size, central directory, entry counts).
Without a fixed ringdown filename and byte size, the upgrade from a status record to a real posterior likelihood artifact cannot start. The module claims structural closure (zero sorry, zero new RS axioms); this entry is one of the five concrete pins that make that claim checkable against Zenodo 7007370.
It does not itself encode RS physics (phi-ladder, J-cost, eight-tick octave). It is verification scaffolding so those claims can later be scored against public GWTC-3 ringdown posteriors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.