guardTestCount
plain-language theorem explainer
Fixes the GWTC-3 ringdown family-guard test suite size at eight discrete model checks. Verification authors cite it when partitioning accepted versus rejected families or packaging the guard certificate. The body is a bare natural-number definition, not a derived count.
Claim. The GWTC-3 ringdown runtime family guard evaluates exactly $8$ named model-family tests.
background
The module formalizes a runtime policy induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. It does not compute posteriors; it only records which model-family strings the guard accepts or rejects.
Accepted families are the three mapped ones: DS one-mode at $10M$, Kerr $(2,2,0)$ at $0M$, and Kerr $(2,2,0)$ at $10M$. Representative blocked or unknown families (Kerr $(2,2,1)$, MMRDNP, pseobnrv4hm, and unknowns) are rejected. Sibling counters track how many of those named checks accept versus reject; this constant is their common total.
proof idea
No proof. The declaration is a definitional abbreviation binding the natural number eight. Downstream lemmas unfold it and discharge equalities by decide.
why it matters
Gives a single named size for the guard suite so the partition theorem can state that accepted-test count plus rejected-test count equals the full suite size, and so the certificate structure can list a fixed battery of accept/reject obligations. In the Recognition verification layer this is structural bookkeeping only: it pins the runtime policy footprint without touching the forcing chain, RCL, or mass ladder. Closure status of the module is zero sorry and zero new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.