guardAcceptedTestCount
plain-language theorem explainer
The runtime family guard accepts exactly three GWTC-3 ringdown model families. Anyone citing the Session 131 stratified selector or the guard certificate uses this constant as the accepted-side cardinality. It is a bare natural-number definition, not a derived count.
Claim. The number of ringdown model families accepted by the GWTC-3 runtime family guard is $3$.
background
The module formalizes a runtime policy induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. It does not evaluate posteriors; it only classifies named model families as accept or reject.
Accepted families are the three mapped ones: the single-mode DS family at $10M$, and the Kerr $(2,2,0)$ families at $0M$ and $10M$. All other listed families (higher multipoles, MMRDNP, pseobnrv4hm, unknowns) are blocked. Sibling counts track eligible, blocked, rejected, and total test families so the guard’s bookkeeping can be checked by partition identities.
proof idea
Definitional constant: the natural number $3$ is assigned directly. No lemmas, tactics, or computation beyond the literal.
why it matters
Pins the accepted-side size used by the partition theorem guardAcceptedTestCount + guardRejectedTestCount = guardTestCount, which discharges by unfolding and decide. The same constant underwrites the certificate structure that packages the three accept facts (DS, Kerr220 at $0M$ and $10M$) with the reject facts for blocked families. In the Recognition verification layer this is structural policy closure only: zero sorry, no new RS axioms, and no claim about likelihood values or mass-ladder physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.