Pith. sign in
module module high

IndisputableMonolith.Verification.GWTC3RingdownZipSchema

show as:
view Lean formalization →

Structural schema for the public GWTC-3 ringdown ZIP (IGWN-GWTC3-TGR-v1-rin.zip): fixed byte sizes, central-directory layout, entry and HDF5 counts, and compressed/uncompressed totals as Lean constants with positivity facts. Verification authors cite it to pin filename taxonomies and sample schemas to one archive fingerprint. Argument is a one-statement schema package over the posterior manifest, not a dynamical proof.

claimThe GWTC-3 ringdown ZIP is fixed by positive integers: source size $S$, central-directory offset $o_{\mathrm{cd}}$ and size $s_{\mathrm{cd}}$, entry count $N$, HDF5 member count $N_{\mathrm{h5}}$, directory-marker and top-level rin counts, and total compressed/uncompressed sizes. These constants form the one-statement archive schema used by downstream ringdown verification.

background

GWTC-3 is the LIGO-Virgo-KAGRA gravitational-wave transient catalog. The ringdown analysis ships as a public Zenodo ZIP (IGWN-GWTC3-TGR-v1-rin.zip) whose members are HDF5 posterior files. Recognition Science verification treats that archive as a frozen artifact: layout and counts must be stated in Lean before any likelihood or taxonomy claim can be machine-checked.

The upstream posterior manifest module records the exact public Zenodo file list needed to upgrade ringdown status from a status record to a real posterior likelihood artifact. This module sits one layer down: it freezes ZIP-level geometry (source size, central-directory offset and size, entry totals, HDF5 vs directory-marker splits, compressed and uncompressed byte sums) without reading sample arrays.

Sibling constants name those integers; companion lemmas assert positivity of source size, central-directory size, and entry count so later modules can treat the archive as a nonempty, well-formed container.

proof idea

Definition-and-schema module, not a multi-step derivation. Numeric layout facts are introduced as named constants (source bytes, central-directory offset/size, entry and HDF5 counts, directory markers, top-level rin count, compressed/uncompressed totals). Short positivity lemmas discharge $S>0$, $s_{\mathrm{cd}}>0$, and $N>0$. No posterior samples are opened; the argument is pure structural recording over the imported posterior manifest.

why it matters in Recognition Science

Pins the archive fingerprint that two structural theorem modules import. The filename taxonomy module records the archive-wide names of the 243 HDF5 files in the ringdown ZIP using only the ZIP central directory, with no posterior samples read. The HDF5 sample-schema module performs the first schema-level inspection of an actual posterior member without downloading the full ~1.44 GB archive. Both closures (0 sorry, 0 RS-internal axiom) rest on this ZIP schema remaining fixed. In the broader verification domain it is the bridge from the Zenodo posterior manifest to concrete ringdown file and sample claims.

scope and limits

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (20)