gwtc3_ringdown_likelihood_selector_one_statement
plain-language theorem explainer
Packages the GWTC-3 ringdown likelihood selector policy into a single conjunction: fixed HDF5 and model-family counts (243/66/177 files, 14/3/11 models), a no-mixed-aggregation flag, and inhabitedness of the selector certificate. Anyone citing the structural closure of the ringdown selector would quote this. The proof is a pure term of seven `rfl`s plus the inhabitedness lemma.
Claim. The selector reports $243$ total HDF5 files, of which $66$ are eligible and $177$ blocked; $14$ model families, of which $3$ are eligible and $11$ blocked; mixed aggregation is disallowed; and the selector certificate structure is inhabited.
background
This module freezes selector policy for future GWTC-3 ringdown likelihood work. It does not compute posteriors. Eligible families are those with a formalized observable map: DS_1mode_10M (direct $f_{t0}/\tau_{t0}$ damping), and Kerr 220 quality-factor maps at $0M$ and $10M$ start. Everything else is blocked until a mapping exists: all Kerr 221 families, all MMRDNP families, and pseobnrv4hm.
The numeric defs are pure constants (selectorTotalHDF5Files = 243, eligible $66$, blocked $177$; models $14/3/11$). The certificate structure GWTC3RingdownLikelihoodSelectorCert packages partition identities (eligible + blocked = total for files and models), alignment of eligible files with the comparison module total, alignment of total files with the taxonomy HDF5 count, and a blocked-files witness. The inhabitedness theorem supplies a concrete inhabitant of that structure.
proof idea
Term-mode proof: a single pair whose first seven components are rfl (each count and the no-mixed-aggregation flag is definitionally equal to the stated numeral or true), and whose last component is gwtc3RingdownLikelihoodSelectorCert_inhabited, which itself is ⟨gwtc3RingdownLikelihoodSelectorCert⟩. No rewriting or case analysis.
why it matters
Closes the selector layer of the GWTC-3 ringdown verification stack as a single quotable statement. Module status is structural theorem: zero sorry, zero new RS-internal axioms, closure dated 2026-05-22. Downstream consumers (none yet wired in this graph) can cite one name rather than seven separate count lemmas plus the certificate. It sits downstream of the family-comparison and filename-taxonomy modules, locking the eligible/blocked partition before any likelihood is formed. Within Recognition Science verification this is bookkeeping, not a forcing-chain step (T0–T8); it gates which ringdown families may later confront RS mass or QNM predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.