Verification Gwtc3 Posterior Manifest

The posterior manifest

The GWTC-3 posterior manifest is a formal record of the exact public data files that a scientific analysis needs. The files come from the LIGO-Virgo-KAGRA collaboration's third gravitational-wave catalog, specifically the data release for tests of general relativity. The manifest names five zip archives stored on the Zenodo repository under record 7007370: files for ringdown tests, inspiral-merger-ringdown consistency, parameterized tests of general relativity, Lorentz-invariance violation, and spin-induced quadrupole moment. Each entry carries its file name, its size in bytes, and an MD5 checksum.

The point of the manifest is precision and completeness. A posterior likelihood analysis is only as trustworthy as the data it consumes, and a missing or corrupted file silently ruins the result. The manifest pins down exactly which files are expected, so a reproducibility script can fetch the same metadata live from the Zenodo API and check that what is on disk matches what the analysis assumes. This is posterior-ingestion preparation, not the posterior likelihood itself.

In Recognition Science, the framework's machine-checked library of formal theorems contains this manifest as a verified structure. The library proves that the manifest is complete: it names exactly five files, the Zenodo record identifier is positive, and every listed file has a positive byte size. A single theorem bundles these facts into one certificate, including the explicit statement that the ringdown file, the one needed for the framework's echo and quasinormal-mode posterior work, is present under its expected name. The proof is checked by the kernel with zero admitted assumptions and zero framework-specific axioms.

What this establishes in plain language is a binding contract between the analysis and the public data. Before any posterior computation can begin, the framework can point to a machine-checked statement that the five required archives are named, sized, and tied to one Zenodo record. The manifest does not analyze gravitational waves; it makes sure the analysis starts from the right, complete, verifiable inputs.

/-- One-statement manifest theorem: the GWTC-3 posterior manifest names
all five expected tests-of-GR zip files, including the ringdown file
required for RS echo/QNM posterior likelihood work. -/
theorem gwtc3_posterior_manifest_one_statement :
    (zenodoRecordId = 7007370) ∧
    (allPosteriorFiles.length = 5) ∧
    (ringdownFile.key = "IGWN-GWTC3-TGR-v1-rin.zip") ∧
    (HasPositiveSize imrFile) ∧
    (HasPositiveSize ringdownFile) ∧
    (HasPositiveSize simFile) ∧
    (HasPositiveSize livFile) ∧
    (HasPositiveSize parFile) ∧
    Nonempty GWTC3PosteriorManifestCert :=
  ⟨rfl,
   posterior_manifest_has_five_files,
   ringdown_file_key,
   imr_size_pos,
   ringdown_size_pos,
   sim_size_pos,
   liv_size_pos,
   par_size_pos,
   gwtc3PosteriorManifestCert_inhabited⟩

theorem posterior_manifest_has_five_files :
    allPosteriorFiles.length = 5 := by
  unfold allPosteriorFiles
  decide

theorem posterior_manifest_record_id_pos : 0 < zenodoRecordId := by
  unfold zenodoRecordId
  decide

theorem imr_size_pos : HasPositiveSize imrFile := by
  unfold HasPositiveSize imrFile
  decide

/-- One-statement manifest theorem: the GWTC-3 posterior manifest names
all five expected tests-of-GR zip files, including the ringdown file
required for RS echo/QNM posterior likelihood work. -/
theorem gwtc3_posterior_manifest_one_statement :
    (zenodoRecordId = 7007370) ∧
    (allPosteriorFiles.length = 5) ∧
    (ringdownFile.key = "IGWN-GWTC3-TGR-v1-rin.zip") ∧
    (HasPositiveSize imrFile) ∧
    (HasPositiveSize ringdownFile) ∧
    (HasPositiveSize simFile) ∧
    (HasPositiveSize livFile) ∧
    (HasPositiveSize parFile) ∧
    Nonempty GWTC3PosteriorManifestCert :=
  ⟨rfl,
   posterior_manifest_has_five_files,
   ringdown_file_key,
   imr_size_pos,
   ringdown_size_pos,
   sim_size_pos,
   liv_size_pos,
   par_size_pos,
   gwtc3PosteriorManifestCert_inhabited⟩

theorem gwtc3PosteriorManifestCert_inhabited :
    Nonempty GWTC3PosteriorManifestCert :=
  ⟨gwtc3PosteriorManifestCert⟩

What this page does not claim

This module does not contain any posterior likelihood computation. This module does not verify the scientific content of the gravitational-wave data. This module does not prove that the Zenodo files are uncorrupted, only that the manifest names them with positive sizes.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/GWTC3PosteriorManifest.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: