selector_model_count_partition
plain-language theorem explainer
Eligible plus blocked GWTC-3 ringdown model families sum to the catalog total: 3 + 11 = 14. Anyone auditing the family-stratified likelihood selector cites this as the model-side partition identity. The proof unfolds the three Nat constants and closes by decidable arithmetic.
Claim. The number of eligible GWTC-3 ringdown model families plus the number of blocked families equals the total number of model families in the selector catalog: $3 + 11 = 14$.
background
The module fixes a structural selector policy for future GWTC-3 ringdown likelihood work. It does not compute posteriors; it only records which waveform families may enter a likelihood and which stay blocked until their observable maps are formalized.
Eligible families are the three with explicit mappings: DS_1mode_10M (direct $f_{t0}/\tau_{t0}$ damping), Kerr_220_0M, and Kerr_220_10M (Kerr 220 quality-factor maps at 0M and 10M start). Blocked families include every Kerr_221*, every MMRDNP*, and pseobnrv4hm, pending formalized mappings. The catalog totals are fixed as Nat constants: 14 model families, of which 3 are eligible and 11 blocked (parallel file counts are 243 total, 66 eligible, 177 blocked).
The three constants used here are pure Nat definitions: eligible models = 3, blocked models = 11, total models = 14.
proof idea
Term-mode proof by unfolding the three Nat definitions and invoking decide. After unfold, the goal is the closed arithmetic fact $3 + 11 = 14$, which Lean discharges by decidable equality on naturals. No lemmas beyond the three constant definitions are required.
why it matters
This is the model-family half of the selector's partition bookkeeping. It is wired directly into gwtc3RingdownLikelihoodSelectorCert as the model_count_partition field, alongside the file-count partition and the cross-checks against the comparison and taxonomy modules.
In the Recognition verification stack this cert is structural hygiene: it locks the published eligible/blocked split (3 of 14 families) so downstream GWTC-3 ringdown likelihood claims cannot silently reclassify Kerr_221*, MMRDNP*, or pseobnrv4hm without breaking the certificate. It is selector policy only, not a physics derivation from the T0–T8 forcing chain, but it is part of the zero-sorry closure path for GWTC-3 ringdown verification artifacts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.