IndisputableMonolith.Verification.GWTC3PosteriorManifest

   1import Mathlib
   2
   3/-!
   4# GWTC-3 Posterior Manifest
   5
   6## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom; closure 2026-05-22).
   7
   8This module records the exact public Zenodo posterior-file manifest
   9needed to upgrade `GWTC3RingdownStatus` from a status record to a real
  10posterior likelihood artifact.
  11
  12Zenodo record:
  13
  14* `7007370`
  15* Title: `Data release for Tests of General Relativity with GWTC-3`
  16
  17Required files:
  18
  19* `IGWN-GWTC3-TGR-v1-rin.zip` — ringdown test posterior files.
  20* `IGWN-GWTC3-TGR-v1-imr.zip` — inspiral-merger-ringdown consistency.
  21* `IGWN-GWTC3-TGR-v1-par.zip` — parameterized GR tests.
  22* `IGWN-GWTC3-TGR-v1-liv.zip` — Lorentz-invariance violation.
  23* `IGWN-GWTC3-TGR-v1-sim.zip` — spin-induced quadrupole moment.
  24
  25The Lean content is the manifest completeness and positivity theorem:
  26the five expected posterior files are named, have positive byte sizes,
  27and are tied to a single Zenodo record id. The companion reproducibility
  28script `papers/reproducibility/gwtc3_posterior_manifest.py` fetches the
  29same metadata live from the Zenodo API and writes JSON/CSV outputs.
  30
  31This is **posterior-ingestion preparation**, not posterior likelihood.
  32Zero `sorry`. Zero new RS-specific axioms.
  33-/
  34
  35namespace IndisputableMonolith
  36namespace Verification
  37namespace GWTC3PosteriorManifest
  38
  39/-! ## §1. Manifest records -/
  40
  41/-- A posterior-file manifest entry. -/
  42structure PosteriorFile where
  43  key : String
  44  sizeBytes : Nat
  45  checksum : String
  46
  47def zenodoRecordId : Nat := 7007370
  48
  49def imrFile : PosteriorFile where
  50  key := "IGWN-GWTC3-TGR-v1-imr.zip"
  51  sizeBytes := 4120399443
  52  checksum := "md5:0a89b6c3d7f43496a4a1b57bb2ac4e32"
  53
  54def ringdownFile : PosteriorFile where
  55  key := "IGWN-GWTC3-TGR-v1-rin.zip"
  56  sizeBytes := 1444203951
  57  checksum := "md5:131d4d5e057f5e1c58787ca2920796a4"
  58
  59def simFile : PosteriorFile where
  60  key := "IGWN-GWTC3-TGR-v1-sim.zip"
  61  sizeBytes := 1317455705
  62  checksum := "md5:fb4ed440b11caf2e0d5b2b4c8c4da707"
  63
  64def livFile : PosteriorFile where
  65  key := "IGWN-GWTC3-TGR-v1-liv.zip"
  66  sizeBytes := 7404733110
  67  checksum := "md5:71575f4a17a5f967fa5903a1f0fbe1b1"
  68
  69def parFile : PosteriorFile where
  70  key := "IGWN-GWTC3-TGR-v1-par.zip"
  71  sizeBytes := 2523809848
  72  checksum := "md5:9a5a1d332e7d47813a7d443e28f27396"
  73
  74def allPosteriorFiles : List PosteriorFile :=
  75  [imrFile, ringdownFile, simFile, livFile, parFile]
  76
  77/-! ## §2. Completeness and positivity -/
  78
  79def HasPositiveSize (f : PosteriorFile) : Prop :=
  80  0 < f.sizeBytes
  81
  82theorem imr_size_pos : HasPositiveSize imrFile := by
  83  unfold HasPositiveSize imrFile
  84  decide
  85
  86theorem ringdown_size_pos : HasPositiveSize ringdownFile := by
  87  unfold HasPositiveSize ringdownFile
  88  decide
  89
  90theorem sim_size_pos : HasPositiveSize simFile := by
  91  unfold HasPositiveSize simFile
  92  decide
  93
  94theorem liv_size_pos : HasPositiveSize livFile := by
  95  unfold HasPositiveSize livFile
  96  decide
  97
  98theorem par_size_pos : HasPositiveSize parFile := by
  99  unfold HasPositiveSize parFile
 100  decide
 101
 102theorem posterior_manifest_has_five_files :
 103    allPosteriorFiles.length = 5 := by
 104  unfold allPosteriorFiles
 105  decide
 106
 107theorem posterior_manifest_record_id_pos : 0 < zenodoRecordId := by
 108  unfold zenodoRecordId
 109  decide
 110
 111/-- Ringdown posterior file is explicitly named in the manifest. -/
 112theorem ringdown_file_key :
 113    ringdownFile.key = "IGWN-GWTC3-TGR-v1-rin.zip" := rfl
 114
 115/-! ## §3. Master cert -/
 116
 117structure GWTC3PosteriorManifestCert where
 118  record_id_pos : 0 < zenodoRecordId
 119  five_files : allPosteriorFiles.length = 5
 120  imr_positive : HasPositiveSize imrFile
 121  ringdown_positive : HasPositiveSize ringdownFile
 122  sim_positive : HasPositiveSize simFile
 123  liv_positive : HasPositiveSize livFile
 124  par_positive : HasPositiveSize parFile
 125  ringdown_named : ringdownFile.key = "IGWN-GWTC3-TGR-v1-rin.zip"
 126
 127def gwtc3PosteriorManifestCert : GWTC3PosteriorManifestCert where
 128  record_id_pos := posterior_manifest_record_id_pos
 129  five_files := posterior_manifest_has_five_files
 130  imr_positive := imr_size_pos
 131  ringdown_positive := ringdown_size_pos
 132  sim_positive := sim_size_pos
 133  liv_positive := liv_size_pos
 134  par_positive := par_size_pos
 135  ringdown_named := ringdown_file_key
 136
 137theorem gwtc3PosteriorManifestCert_inhabited :
 138    Nonempty GWTC3PosteriorManifestCert :=
 139  ⟨gwtc3PosteriorManifestCert⟩
 140
 141/-- One-statement manifest theorem: the GWTC-3 posterior manifest names
 142all five expected tests-of-GR zip files, including the ringdown file
 143required for RS echo/QNM posterior likelihood work. -/
 144theorem gwtc3_posterior_manifest_one_statement :
 145    (zenodoRecordId = 7007370) ∧
 146    (allPosteriorFiles.length = 5) ∧
 147    (ringdownFile.key = "IGWN-GWTC3-TGR-v1-rin.zip") ∧
 148    (HasPositiveSize imrFile) ∧
 149    (HasPositiveSize ringdownFile) ∧
 150    (HasPositiveSize simFile) ∧
 151    (HasPositiveSize livFile) ∧
 152    (HasPositiveSize parFile) ∧
 153    Nonempty GWTC3PosteriorManifestCert :=
 154  ⟨rfl,
 155   posterior_manifest_has_five_files,
 156   ringdown_file_key,
 157   imr_size_pos,
 158   ringdown_size_pos,
 159   sim_size_pos,
 160   liv_size_pos,
 161   par_size_pos,
 162   gwtc3PosteriorManifestCert_inhabited⟩
 163
 164end GWTC3PosteriorManifest
 165end Verification
 166end IndisputableMonolith
 167