PosteriorFile
plain-language theorem explainer
Records one GWTC-3 Zenodo posterior archive as a named triple: filename key, byte size, and checksum string. Downstream manifest completeness and positivity proofs cite this carrier type when listing the five TGR posterior zips. Pure structure definition; no proof obligation.
Claim. A posterior-file manifest entry is a triple $(k, n, c)$ with filename key $k$ a string, size $n \in \mathbb{N}$ in bytes, and checksum $c$ a string (typically an MD5 tag).
background
The module freezes the public Zenodo record 7007370 (Data release for Tests of General Relativity with GWTC-3) so that ringdown and related TGR status objects can later attach real posterior likelihood artifacts rather than bare status flags.
Required archives are the five IGWN-GWTC3-TGR-v1 zips: ringdown (rin), inspiral-merger-ringdown consistency (imr), parameterized GR tests (par), Lorentz-invariance violation (liv), and spin-induced quadrupole (sim). This structure is the common carrier for each archive's identity metadata.
The Lean layer is posterior-ingestion preparation only: named files, positive sizes, one record id. A companion Python script re-fetches the same Zenodo API metadata for external reproducibility.
proof idea
No proof. The declaration is a structure with three fields (key, sizeBytes, checksum). Instances such as the IMR and ringdown file constants fill the fields with concrete strings and natural numbers; positivity and list-completeness theorems then quantify over those instances.
why it matters
Gives a uniform type for every GWTC-3 TGR posterior zip so the module can state a single completeness list (allPosteriorFiles) and a single positivity predicate (HasPositiveSize). Concrete file constants (imrFile, ringdownFile, simFile, livFile, parFile) inhabit this type and feed the structural theorem that the five expected archives are named, nonempty in bytes, and tied to Zenodo 7007370.
That theorem upgrades GWTC-3 ringdown status from a status record toward a real posterior likelihood artifact. It does not yet compute likelihoods; it closes the manifest bookkeeping with zero sorry and no new RS axioms. Framework role is verification plumbing for gravitational-wave TGR tests, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.