guard_rejects_unknown
plain-language theorem explainer
The ringdown family guard maps any unrecognized model-family string to reject. Verification authors cite it to show the Session-131 runtime policy blocks unknown GWTC-3 families, not only the named blocked ones. The proof is a two-step unfold-and-simp evaluation of the decision table on the concrete string "not_a_real_family".
Claim. Evaluating the GWTC-3 ringdown family guard on the unrecognized family name $\texttt{not\_a\_real\_family}$ yields the reject decision.
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 accepts three mapped families (DS_1mode_10M, Kerr_220_0M, Kerr_220_10M) and rejects blocked or unknown families, without computing any posterior likelihood.
The decision function guardModel is a pure string-to-decision table returning an accept/reject enum. Sibling lemmas cover the three accepts and several named rejects (Kerr_221_0M, Kerr_221_domega_221_0M, MMRDNP_10M, pseobnrv4hm). This lemma is the catch-all for strings outside that enumerated set.
Module status is a closed structural theorem: zero sorry, zero new RS-specific axioms.
proof idea
Term-mode computational check. Unfold the definition of the guard decision table, then simp reduces the match on the concrete unrecognized string to the default reject branch. No external lemmas are required beyond definitional equality.
why it matters
Closes the unknown-family case in the guard's accept/reject partition. Downstream, gwtc3RingdownFamilyGuardCert packages the three accepts and the named rejects into a single certificate record; this lemma is the natural witness that strings outside the mapped set are rejected, completing the runtime-policy story the certificate advertises.
In the broader Verification domain this is not a physics derivation (no T5–T8 forcing, no mass ladder). It is audit infrastructure: a machine-checked statement that the GWTC-3 ringdown selector will not silently accept an unmapped family name at runtime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.