parFile
plain-language theorem explainer
Records the Zenodo posterior archive for parameterized tests of GR in GWTC-3: filename, byte size, and MD5. Anyone wiring GWTC-3 TGR posteriors into a Lean manifest or reproducibility check cites this entry. It is a pure structure literal, no proof obligations.
Claim. The parameterized-GR posterior package is the manifest entry with key $\texttt{IGWN-GWTC3-TGR-v1-par.zip}$, size $2523809848$ bytes, and checksum $\texttt{md5:9a5a1d332e7d47813a7d443e28f27396}$.
background
The module freezes the public Zenodo release (record 7007370, "Data release for Tests of General Relativity with GWTC-3") as a Lean manifest. That release supplies five zip archives covering ringdown, IMR consistency, parameterized GR deviations, Lorentz-invariance violation, and spin-induced quadrupole tests. The goal is posterior-ingestion preparation for upgrading ringdown status records into real likelihood artifacts, not the likelihoods themselves.
A posterior-file entry is a triple: string key (archive name), natural-number size in bytes, and checksum string. This definition is the parameterized-GR member of that family. Sibling entries cover the other four archives; together they feed the completeness and positivity theorems for the full five-file list.
proof idea
Definitional structure instance. The three fields of the posterior-file record are filled by string and natural literals (key, sizeBytes, checksum). No tactics, no lemmas, no computation beyond the literal assignment.
why it matters
Closes one of the five required TGR posterior slots named in the module doc. It is listed in the full posterior-file collection, supplies the positivity witness for the parameterized archive, and appears in the master certificate structure and the one-statement manifest theorem (Zenodo id, five files, named ringdown key, positive sizes). Without this entry the manifest would be incomplete for parameterized GR tests, blocking the path from structural status records to ingested GWTC-3 posteriors used in RS echo/QNM likelihood work. Zero sorry; pure data binding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.