guard_test_count_partition
plain-language theorem explainer
The eight ringdown-family guard tests partition cleanly into three accepted and five rejected cases: 3 + 5 = 8. Anyone citing the GWTC-3 family-guard certificate uses this as the arithmetic sanity check that the test suite is exhaustive and non-overlapping. The proof unfolds the three Nat constants and closes by decide.
Claim. The number of accepted guard tests plus the number of rejected guard tests equals the total number of guard tests: $3 + 5 = 8$.
background
The module formalizes a runtime family guard induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. It is structural policy only: it records which model families the selector admits and which it blocks, and it computes no posterior likelihood.
Three Nat constants count the fixed test suite: total tests equal 8, accepted tests equal 3 (the mapped families DS_1mode_10M, Kerr_220_0M, Kerr_220_10M), and rejected tests equal 5 (Kerr_221_0M, Kerr_221_domega_221_0M, MMRDNP_10M, pseobnrv4hm, and unknown). Sibling lemmas prove each individual accept/reject decision; this theorem only checks that those counts add up.
proof idea
Term-mode proof by unfolding the three definitions guardAcceptedTestCount, guardRejectedTestCount, and guardTestCount to the literals 3, 5, and 8, then closing with decide on the ground equality 3 + 5 = 8. No lemmas beyond the definitions are required.
why it matters
Feeds the certificate bundle gwtc3RingdownFamilyGuardCert, which packages the three accept lemmas and the reject lemmas into a single structured witness that the runtime guard matches the Session 131 selector policy. Without the partition identity, a referee could worry that the suite under- or over-counts relative to the listed families. The result is pure bookkeeping inside the Verification domain; it does not touch the RS forcing chain (T0–T8), RCL, or mass-ladder physics. It closes one arithmetic obligation in a zero-sorry structural theorem module dated 2026-05-22.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.