Pith. sign in
module module high

IndisputableMonolith.Verification.GWTC3RingdownLikelihoodSelector

show as:
view Lean formalization →

Records a one-statement likelihood selector over the GWTC-3 ringdown HDF5 archive: files and models partition into eligible versus blocked sets under the controlled damping families. Verification authors cite it when locking which ringdown posteriors may enter a family-stratified comparison. The argument is structural bookkeeping: counts match the filename taxonomy and the mapped-family comparison, with an explicit no-mixed-aggregation clause.

claimOver the GWTC-3 ringdown archive of $N$ HDF5 files, the selector partitions files into eligible and blocked sets $E_f \sqcup B_f$ and models into $E_m \sqcup B_m$, with $|E_f|+|B_f|=N$ and likewise for models. Eligible files coincide with those admitted by the controlled-family comparison; total file count matches the filename taxonomy. Mixed aggregation across unmapped families is forbidden.

background

The setting is structural verification of the public GWTC-3 ringdown release (IGWN-GWTC3-TGR-v1-rin.zip), not a new gravitational-wave measurement. Upstream, the filename taxonomy module catalogs all 243 HDF5 entries from the ZIP central directory alone, without reading posterior samples. The family-comparison module aggregates the currently mapped damping families (including DS_1mode_10M and Kerr_220_0M) into a controlled comparison surface.

This selector sits between those two layers. It names total, eligible, and blocked counts for both files and models, and asserts that the eligible slice is exactly the comparison-admitted set while the total matches the taxonomy. The design goal is a single, citable partition statement rather than ad hoc filename filters scattered through later proofs.

proof idea

The module is a thin structural layer over the taxonomy and family-comparison imports. File and model counts are defined as totals, eligible subsets, and blocked complements. Partition lemmas show the two sides sum to the totals. Alignment lemmas identify eligible files with the comparison module's admitted set and total files with the taxonomy count. A separate clause records that mixed aggregation across unmapped families is disallowed, and that the blocked set is nonempty. No analytic GW likelihood is derived here; the work is equality and disjoint-union bookkeeping.

why it matters in Recognition Science

Downstream, the runtime family guard imports this selector as the Session 131 family-stratified likelihood gate: the guard accepts only the three mapped model families induced by the selector. Without a single partition theorem, later verification could silently mix blocked filenames into ringdown likelihood stacks. In the Recognition Science verification stack this is infrastructure, not a forcing-chain step (T0–T8); it keeps external GWTC-3 evidence claims pinned to an explicit, machine-checked eligibility cut rather than informal file lists.

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)