GWTC3RingdownLikelihoodSelectorCert
plain-language theorem explainer
Certificate bundling the GWTC-3 ringdown likelihood selector policy: eligible vs blocked file and model counts partition the catalog, eligible files match the family-comparison total (66), totals match the filename taxonomy (243), some files are blocked, and mixed aggregation is forbidden. Downstream family-guard and one-statement selector theorems inhabit and cite it. The structure is pure packaging of Nat equalities and Nonempty witnesses already proved as sibling lemmas.
Claim. A selector certificate is a record asserting: (i) eligible plus blocked HDF5 files equal the selector total; (ii) eligible plus blocked model families equal the model total; (iii) the eligible-file count equals the family-comparison member total; (iv) the selector file total equals the taxonomy HDF5 count; (v) at least one file is blocked; (vi) mixed aggregation is disallowed; (vii) a family-comparison certificate exists; (viii) a filename-taxonomy certificate exists.
background
The module fixes a structural selector policy for future GWTC-3 ringdown likelihood work. It does not compute posteriors. Mapped (eligible) families are the direct damped-sinusoid DS_1mode_10M and the Kerr-220 quality-factor maps at 0M and 10M start. Everything in Kerr_221*, MMRDNP*, and pseobnrv4hm stays blocked until the corresponding observable or waveform-family maps are formalized.
Numeric anchors come from sibling defs and upstream modules: taxonomy reports 243 HDF5 files; family comparison reports 66 total members across the three eligible families; the selector records 177 blocked files and 11 blocked model families (3 eligible of 14). Upstream GWTC3RingdownFamilyComparisonCert partitions those 66 members and their sample counts; GWTC3RingdownFilenameTaxonomyCert partitions the 243 files by pipeline and category and ties the count to the ringdown zip inventory.
proof idea
No proof body: this is a structure (certificate type), not a theorem. Each field is a Prop-valued obligation. The concrete inhabitant gwtc3RingdownLikelihoodSelectorCert fills those fields by pointing at the sibling lemmas selector_file_count_partition, selector_model_count_partition, selector_eligible_files_match_comparison, selector_total_files_match_taxonomy, and the analogous facts for blocked files, no mixed aggregation, and Nonempty witnesses for the comparison and taxonomy certificates. Those lemmas are ordinary Nat arithmetic on the closed constants 66, 177, 243, 3, 11, 14.
why it matters
This certificate is the policy hinge between catalog taxonomy, family comparison, and runtime guarding. GWTC3RingdownFamilyGuardCert consumes the same accept/reject split (accept the three mapped families; reject Kerr-221 and MMRDNP exemplars). The module closes with gwtc3RingdownLikelihoodSelectorCert_inhabited and the one-statement theorem that packages the explicit counts (243/66/177 files, 14/3/11 models). In the Verification domain it records what may enter a future ringdown likelihood without claiming any RS mass-ladder, alpha-band, or forcing-chain (T0–T8) physics. Status note: structural theorem layer, zero sorry, zero new RS axioms; selector policy only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.