Pith. sign in
module module moderate

IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy

show as:
view Lean formalization →

Records a one-statement filename taxonomy of the GWTC-3 ringdown ZIP central directory: event counts, waveform-family tallies (Pyring, SEOBNRv4HM, Kerr, MMRDNP, damped sinusoid), and compressed/uncompressed size extremes. Downstream ringdown damping-family and likelihood-selector modules import these counts as fixed structural facts. The argument is a pure enumeration over the already-certified ZIP schema, with no analytic content.

claimThe GWTC-3 ringdown archive $IGWN$-$GWTC3$-$TGR$-$v1$-$rin.zip$ admits a fixed filename taxonomy: $N_{\mathrm{HDF5}}$ member files, $N_{\mathrm{evt}}$ events, and family counts $N_{\mathrm{Pyring}}$, $N_{\mathrm{SEOBNR}}$, $N_{\mathrm{Kerr}}$, $N_{\mathrm{MMRDNP}}$, $N_{\mathrm{DS}}$, $N_{\mathrm{wf}}$, together with total compressed and uncompressed byte sizes and the extremal members by size.

background

GWTC-3 is the LIGO-Virgo-KAGRA gravitational-wave transient catalog. The ringdown release packages posterior samples and waveform reconstructions for tests of general relativity in the quasinormal-mode (QNM) regime. The upstream module GWTC3RingdownZipSchema certifies the ZIP central-directory layout of IGWN-GWTC3-TGR-v1-rin.zip from an HTTP range request only (no full 1.44 GB payload), and is marked a structural theorem with zero sorry and zero RS-internal axioms.

This module sits one layer above that schema. It does not re-derive the directory bytes; it classifies every listed member by filename pattern into event identifiers and analysis families (Pyring, SEOBNRv4HM, Kerr, MMRDNP, damped-sinusoid, generic waveform). The sibling constants expose the resulting integer tallies and the smallest/largest members by compressed size. The setting is pure verification bookkeeping inside the Recognition Science monolith, not a derivation from the J-cost or the forcing chain.

proof idea

Definition-and-enumeration module, not an analytic proof. It imports the certified ZIP central-directory schema, pattern-matches each filename into a disjoint family bucket, and records the bucket cardinalities and size aggregates as named constants (HDF5 file count, event count, per-family counts, total compressed/uncompressed size, extremal members). The "one-statement filename-taxonomy theorem" packages those equalities into a single structural claim. No tactic reasoning beyond reflexivity on the schema data is required.

why it matters in Recognition Science

Gives every controlled-family ringdown statistic a fixed, machine-checked denominator and eligibility set. Three immediate consumers import it: the DS_1mode_10M damping-family module (first controlled-family scaling of the Session 123 one-member QNM damping statistic), the Kerr_220_0M damping-family module (first controlled Kerr-family scaling of the same statistic), and the family-stratified likelihood selector (selector policy for future GWTC-3 ringdown likelihoods, with mapped/eligible families). Without the taxonomy, those modules could not state which archive members enter each family or prove that the family partitions are exhaustive relative to the ZIP schema. The module is structural verification infrastructure, not a physics claim about QNM frequencies or Recognition-ladder masses.

scope and limits

used by (3)

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 (25)