simFile
plain-language theorem explainer
Names the GWTC-3 spin-induced quadrupole (SIM) posterior zip as a typed manifest entry: filename, byte size, and MD5. Verification and RS echo/QNM pipelines cite it when assembling the five-file TGR posterior set from Zenodo 7007370. The body is a pure structure literal; no proof obligations.
Claim. The spin-induced quadrupole posterior artifact is the manifest entry with key $\texttt{IGWN-GWTC3-TGR-v1-sim.zip}$, size $1317455705$ bytes, and checksum $\texttt{md5:fb4ed440b11caf2e0d5b2b4c8c4da707}$.
background
The module freezes the public Zenodo posterior-file manifest for GWTC-3 tests of GR (record 7007370), so ringdown and related status records can be upgraded to real posterior likelihood artifacts. It is posterior-ingestion preparation only: named files, positive sizes, one record id; not a likelihood evaluation.
A posterior-file entry is a triple: string key (zip name), natural-number size in bytes, and checksum string. Five zips are required: IMR consistency, ringdown, parameterized GR, Lorentz-invariance violation, and spin-induced quadrupole moment (this entry).
Companion script gwtc3_posterior_manifest.py re-fetches the same metadata live from the Zenodo API for external reproducibility checks.
proof idea
Definitional structure instance of PosteriorFile. The three fields are set by literals: key string, sizeBytes natural, and MD5 checksum string. No tactics, no lemmas, no computation beyond the literal assignment.
why it matters
Fills the SIM slot in the five-file TGR manifest. It is listed in allPosteriorFiles, supplies the sim_positive field of GWTC3PosteriorManifestCert, and is discharged by sim_size_pos (HasPositiveSize via decide). The one-statement theorem gwtc3_posterior_manifest_one_statement conjoins record id, length five, ringdown key, and positivity of all five files, including this one.
Within Recognition Science verification this is structural closure for GWTC-3 posterior ingestion (module status: 0 sorry, 0 RS-internal axioms). It does not itself encode RS mass-ladder or J-cost physics; it anchors the external LIGO/Virgo/KAGRA TGR data release so later echo/QNM likelihood work has a pinned artifact name and hash.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.