gwtc3RingdownLikelihoodSelectorCert
plain-language theorem explainer
Packages the GWTC-3 ringdown likelihood selector policy as one certificate: eligible and blocked HDF5 files and model families partition the totals, eligible files match the controlled-family comparison count, totals match the filename taxonomy, blocked files are nonempty, mixed aggregation is forbidden, and both upstream certificates are inhabited. Verification authors cite it as the one-shot selector bundle. The body is a structure literal wiring eight already-proved facts.
Claim. A selector certificate exists whose fields assert: eligible plus blocked HDF5 files equal the catalog total ($66+177=243$); eligible plus blocked model families equal the family total ($3+11=14$); the eligible-file count equals the controlled-family comparison membership total; the total file count equals the taxonomy HDF5 count; the blocked-file count is strictly positive; mixed aggregation is disallowed; and both the family-comparison and filename-taxonomy certificates are inhabited.
background
This module records selector policy for future GWTC-3 ringdown likelihoods. It does not evaluate posteriors. Mapped (eligible) families are the direct damping map DS_1mode_10M and the Kerr-220 quality-factor maps at 0M and 10M start. Blocked until formalized: every Kerr-221 family, every MMRDNP family, and pseobnrv4hm.
Numeric anchors fixed in the module: 243 HDF5 files (66 eligible, 177 blocked) and 14 model families (3 eligible, 11 blocked). The certificate structure demands six arithmetic or policy equalities plus two inhabited upstream certificates: the controlled-family comparison bundle and the filename-taxonomy bundle.
Upstream, the comparison and taxonomy modules each expose a one-statement inhabited certificate. Sibling lemmas already prove the partitions by decide, the eligible-file match by rfl, positivity of blocked files, and the no-mixed-aggregation flag.
proof idea
Pure structure construction. Each field of the certificate is filled by a named sibling theorem or an upstream inhabited certificate: file and model count partitions, eligible-files match to comparison membership, total-files match to taxonomy count, blocked-files positivity, the no-mixed-aggregation truth, plus the nonempty comparison and taxonomy certificates. No new reasoning; the def is the wiring.
why it matters
Closes the selector layer of the GWTC-3 ringdown verification stack as a single inhabitable object. Downstream, the one-statement selector theorem is exactly Nonempty of this certificate, obtained by packing this def. Module status is structural theorem: zero sorry, zero new RS-internal axioms, closure dated 2026-05-22.
In the broader Recognition verification program this is bookkeeping, not dynamics: it freezes which waveform families may enter a future ringdown likelihood and which stay blocked until their observable maps are formalized. It does not touch the forcing chain (T0–T8), J-cost, or the mass ladder; it only gates external GW catalog inputs so later likelihood claims cannot silently mix unmapped families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.