guardEligibleModelCount
plain-language theorem explainer
The runtime family guard admits exactly three GWTC-3 ringdown model families. Anyone checking the Session 131 selector against the guard cites this constant. It is a bare natural-number definition equal to three, matching the three accepted labels DS_1mode_10M, Kerr_220_0M, and Kerr_220_10M.
Claim. The number of model families accepted by the GWTC-3 ringdown runtime family guard is the natural number $3$.
background
The module formalizes a runtime policy guard induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. It does not compute posteriors; it only records which named model families the guard accepts or rejects.
Accepted families are exactly three: the single-mode damped-sinusoid family DS_1mode_10M, and the two Kerr $(2,2,0)$ families at $0M$ and $10M$ start times. Representative blocked families include Kerr $(2,2,1)$, MMRDNP, pseobnrv4hm, and unknown labels. Sibling definitions package accept/reject decisions and a matching blocked-model count.
This constant is the eligible side of that bookkeeping: a fixed Nat equal to the size of the accepted set, so downstream certificates can assert count agreement without re-enumerating strings.
proof idea
No proof. The declaration is a definitional abbreviation: the natural number literal $3$. Downstream theorems unfold it and discharge equalities by rfl or simp against the selector's eligible-model count and the guarded-script count.
why it matters
It anchors the quantitative half of the family-guard certificate. The theorem guard_counts_match_selector equates this constant to the selector's eligible-model count (and pairs it with the blocked count). The structure GWTC3RingdownFamilyGuardCert packages the three accepts and the rejects; the count makes the cardinality of that accept set an explicit, checkable fact.
In the guarded-scripts layer, guarded_script_count_matches_selector is definitional equality of the script count with this constant, and GWTC3RingdownGuardedFamilyScriptsCert records that equality beside smoke-test flags. Within Recognition Science verification this is structural policy formalization only (zero sorry, no new RS axioms): it locks the three-family accept list so ringdown claims cannot silently widen the model set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.