Pith. sign in
module module high

IndisputableMonolith.Verification.GWTC3RingdownLikelihoodSelector

show as:
view Lean formalization →

Module that packages a one-statement likelihood selector over the GWTC-3 ringdown HDF5 archive: files and models are partitioned into eligible versus blocked sets under a fixed family taxonomy. Verification authors cite it when they need certified counts and the no-mixed-aggregation invariant before any posterior is read. The argument is structural bookkeeping against the filename taxonomy and the controlled-family comparison, not a statistical fit.

claimOver the GWTC-3 ringdown archive of $N=243$ HDF5 files, the selector partitions files and models into eligible and blocked sets so that $N = N_{\mathrm{elig}} + N_{\mathrm{block}}$ (and likewise for models), with no mixed aggregation across families. Eligible files match the controlled-family comparison; totals match the filename taxonomy; the blocked set is nonempty.

background

GWTC-3 ringdown verification in this tree is deliberately sample-free at the taxonomy layer. The filename taxonomy module records an archive-wide classification of the 243 HDF5 entries in IGWN-GWTC3-TGR-v1-rin.zip from the ZIP central directory alone; no posterior samples are opened. That gives a fixed universe of files and model tags against which any selector can be checked for completeness and partition.

The controlled-family comparison module aggregates the currently mapped damping families (including DS_1mode_10M and Kerr_220_0M) into a structural comparison object. Eligibility here means membership in that mapped family set under the Session 131 family-stratified likelihood policy, not a likelihood-ratio threshold on data.

This selector module sits between those two layers: it names the total, eligible, and blocked counts for files and for models, asserts the partition identities, and ties eligible files to the comparison and totals to the taxonomy.

proof idea

Structural, not analytic. Counts and set names are defined from the taxonomy and family-comparison imports; partition lemmas are ordinary finite-set cardinality identities (eligible disjoint blocked, union recovers the total). Matching lemmas are equality of the selector's eligible-file set with the comparison's mapped set, and equality of the selector's total with the taxonomy's archive size. A separate fact records that the blocked set is nonempty, so the selector is not the trivial all-pass filter. No sorry and no RS-internal axioms; closure is pure bookkeeping over the imported structural theorems.

why it matters in Recognition Science

Downstream, the runtime family guard imports this module as the certified source of the Session 131 family-stratified likelihood selector. The guard accepts only the three mapped model families; without a proved eligible/blocked partition and the no-mixed-aggregation invariant, that guard would be an untracked filter rather than a structural theorem.

In the broader Recognition verification stack this is infrastructure, not a physics claim about ringdown spectra or the forcing chain (T0–T8). It freezes which GWTC-3 ringdown products may enter later family-level comparisons so that any subsequent RS-facing statement about damping families cannot silently mix unmapped filenames or models. Parent consumers should treat the selector counts as the authoritative pre-likelihood cut.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (17)