sim_size_pos
plain-language theorem explainer
The spin-induced quadrupole (SIM) GWTC-3 posterior zip is recorded with a strictly positive byte size on the Zenodo 7007370 manifest. Anyone assembling the five-file completeness certificate or the one-statement posterior-manifest theorem cites this fact. The proof unfolds the positivity predicate on the fixed SIM entry and discharges the numeric inequality by decision procedure.
Claim. The SIM posterior-file entry with key $\mathrm{IGWN\text{-}GWTC3\text{-}TGR\text{-}v1\text{-}sim.zip}$ and size $1317455705$ bytes has strictly positive size: $0 < \mathrm{sizeBytes}$.
background
This module is posterior-ingestion preparation for GWTC-3 tests of GR, not a likelihood computation. It freezes the public Zenodo record 7007370 (Data release for Tests of General Relativity with GWTC-3) and the five expected zip keys: ringdown, IMR consistency, parameterized GR, Lorentz-invariance violation, and spin-induced quadrupole (SIM).
A posterior-file entry is a triple of string key, natural-number byte size, and checksum string. Positivity of an entry means its byte size is strictly greater than zero. The SIM entry is the fixed structure with key IGWN-GWTC3-TGR-v1-sim.zip, size 1317455705, and the recorded MD5 checksum.
Sibling positivity lemmas cover the IMR and ringdown zips the same way. Together they feed the structural claim that the manifest names five non-empty files tied to one record id.
proof idea
Term-mode proof by unfolding. Expand the positivity predicate to the inequality $0 < f.\mathrm{sizeBytes}$, then expand the SIM file definition so the size becomes the concrete natural 1317455705. The tactic decide closes the ground inequality by computation. No external lemmas beyond the local definitions are required.
why it matters
The certificate structure wires this lemma in as the SIM positivity field, alongside IMR and ringdown positivity, five-file count, and positive record id. The one-statement theorem packages the same facts into a single conjunction that names all five expected tests-of-GR zips, including the ringdown file needed for later RS echo/QNM posterior likelihood work.
In the Recognition verification stack this is structural closure only: it upgrades a status record toward a real posterior artifact by pinning public file metadata. It does not touch the forcing chain (T0–T8), the J-cost, or mass-ladder physics; it is infrastructure so those analyses can cite a machine-checked manifest rather than an informal file list. Companion Python reproducibility code fetches the same Zenodo metadata live.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.