guardRejectedTestCount
plain-language theorem explainer
The GWTC-3 ringdown family guard records five rejected test cases in its fixed acceptance suite. Anyone citing the runtime policy partition or the guard certificate uses this constant as the rejected-side count. It is a bare natural-number definition equal to five, matching the five blocked or unknown families named in the module.
Claim. The number of rejected test cases in the GWTC-3 ringdown runtime family guard is the natural number $5$.
background
The module formalizes a runtime family guard induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. The guard is pure policy: it maps model-family name strings to accept or reject and computes no posterior likelihood.
Accepted families are exactly three: DS one-mode at 10M, Kerr 220 at 0M, and Kerr 220 at 10M. Rejected representatives are Kerr 221 at 0M, Kerr 221 with frequency shift, MMRDNP at 10M, pseobnrv4hm, and any unknown model string. The rejected-test count is the size of that blocked side of the fixed test suite.
Sibling counts (eligible, blocked, accepted, total) live in the same module and are used only for structural bookkeeping of the guard, not for physics inference.
proof idea
No proof. The declaration is a definition that sets the natural number equal to five by direct assignment. Downstream theorems unfold it and discharge equalities by decide.
why it matters
The constant feeds the partition theorem that accepted plus rejected test counts equal the total test count, and it appears in the fields of the GWTC-3 ringdown family guard certificate structure (which packages the three accepts and the representative rejects). Together those results close the structural claim that the runtime policy accepts only the three mapped families and rejects the blocked or unknown ones, with zero sorry and no new RS-specific axioms. It is verification scaffolding for the ringdown selector, not a step in the T0–T8 forcing chain or a mass or coupling derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.