module module high

`IndisputableMonolith.Verification.GWTC3PosteriorManifest`

Catalog of named GWTC-3 posterior data files (IMR, ringdown, SIM, LIV, parameter) with Zenodo record id and positive-size witnesses. Verification authors cite it when wiring ZIP-schema or TGR checks to fixed external artifacts. The module is pure data and size predicates; no physics derivation.

claimA finite manifest of GWTC-3 posterior files: each entry is a named file path under a fixed Zenodo record, together with predicates asserting that the IMR, ringdown, SIM (and related) files have strictly positive byte size. The collection $F = \{f_{\mathrm{IMR}}, f_{\mathrm{rd}}, f_{\mathrm{SIM}}, \ldots\}$ is the closed list used by downstream ZIP-schema verification.

background

GWTC-3 is the LIGO–Virgo–KAGRA gravitational-wave transient catalog (O3). Recognition Science verification modules pin external data products so that ringdown and tests-of-GR claims can cite a fixed, auditable artifact set rather than ad-hoc downloads.

This module introduces a posterior-file manifest entry type and concrete names for the IMR, ringdown, SIM, LIV, and parameter posterior files under one Zenodo record id. It also packages the closed list of those files and elementary positive-size predicates (byte length strictly greater than zero) for the principal members.

The local setting is structural verification only: Mathlib is imported for basic types and arithmetic; no Recognition forcing chain, J-cost, or mass-ladder material appears here.

proof idea

This is a definition and data module, not a proof module. It declares a manifest entry structure, string constants for the Zenodo record and each posterior filename, an aggregated list of those files, a positive-size predicate, and a handful of trivial size-positivity facts for the main files. There is no tactic proof burden beyond those size witnesses.

why it matters in Recognition Science

Downstream, GWTC3RingdownZipSchema imports this manifest so that the structural theorem for the central directory of IGWN-GWTC3-TGR-v1-rin.zip can name the same posterior artifacts the HTTP range-request schema is checked against. Without a single closed file list and size witnesses, ZIP-schema and TGR verification would float free of the published GWTC-3 release. The module therefore anchors the verification domain’s data layer; it does not itself advance T0–T8 or the Recognition Composition Law.

scope and limits

Does not parse or validate ZIP central-directory bytes.
Does not download or hash the 1.44 GB payload.
Does not claim scientific correctness of GWTC-3 posteriors.
Does not derive ringdown frequencies or TGR bounds.
Does not connect to phi-ladder, J-cost, or forcing chain T0–T8.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Verification.GWTC3RingdownZipSchema module_import

declarations in this module (21)

structure PosteriorFile L42
def zenodoRecordId L47
def imrFile L49
def ringdownFile L54
def simFile L59
def livFile L64
def parFile L69
def allPosteriorFiles L74
def HasPositiveSize L79
theorem imr_size_pos L82
theorem ringdown_size_pos L86
theorem sim_size_pos L90
theorem liv_size_pos L94
theorem par_size_pos L98
theorem posterior_manifest_has_five_files L102
theorem posterior_manifest_record_id_pos L107
theorem ringdown_file_key L112
structure GWTC3PosteriorManifestCert L117
def gwtc3PosteriorManifestCert L127
theorem gwtc3PosteriorManifestCert_inhabited L137
theorem gwtc3_posterior_manifest_one_statement L144