guardBlockedModelCount
plain-language theorem explainer
Fixes the blocked-family census of the GWTC-3 ringdown runtime guard at the natural number 11. Verification authors cite it when checking that the guard’s reject list has the same cardinality as the Session 131 likelihood selector’s blocked set. It is a bare numeric definition, not a derived theorem.
Claim. Under the GWTC-3 ringdown runtime family guard, the number of blocked (rejected or unknown) model families is the natural number $11$.
background
The module formalizes a runtime policy induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. The guard is a pure accept/reject map on model-family names: it accepts only three mapped families (DS_1mode_10M, Kerr_220_0M, Kerr_220_10M) and rejects every other named family, including representative blocked families such as Kerr_221_0M, Kerr_221_domega_221_0M, MMRDNP_10M, pseobnrv4hm, and unknown labels.
This declaration is the blocked-side census constant paired with the eligible-side count. The module computes no posterior likelihood; it only records the structural accept/reject policy with zero sorry and no new RS-specific axioms.
proof idea
No proof. The declaration is a definition that binds the natural-number constant $11$. Downstream equality with the selector’s blocked-model count is discharged by unfolding both sides and simplifying.
why it matters
Supplies the blocked cardinality half of the census identity guard_counts_match_selector, which asserts that the guard’s eligible and blocked counts equal the selector’s corresponding constants. That identity, together with the per-family accept/reject lemmas, populates the certificate structure GWTC3RingdownFamilyGuardCert used to package the runtime policy as a checkable artifact. In the broader Verification domain this is structural bookkeeping only: it locks the size of the reject list so the guard cannot silently drift from the Session 131 selector without breaking the equality theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.