guardModel
plain-language theorem explainer
Maps a GWTC-3 ringdown model-family name to accept or reject under the Session 131 family-stratified likelihood selector. Only three mapped families (DS one-mode at 10M, Kerr 220 at 0M, Kerr 220 at 10M) are accepted; every other string is rejected. Verification authors cite it when fixing which ringdown templates are runtime-eligible. The body is a three-branch string-equality cascade with default reject.
Claim. Given a model-family name $m$ (as a string), return $\mathrm{accept}$ if $m \in \{\mathrm{DS\_1mode\_10M},\,\mathrm{Kerr\_220\_0M},\,\mathrm{Kerr\_220\_10M}\}$, and $\mathrm{reject}$ otherwise.
background
The module formalizes the runtime family guard induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. Status is structural: zero sorry, zero new RS-internal axioms. It records policy only and never evaluates a posterior likelihood.
GuardDecision is a two-constructor inductive type with values accept and reject (decidable equality). The guard is the function that classifies a model-family string into that type. Accepted families are exactly the three mapped ones listed in the module doc: DS one-mode at 10M, Kerr 220 starting at 0M, and Kerr 220 starting at 10M. Representative blocked families include Kerr 221, Kerr 221 with frequency shift, MMRDNP, pseobnrv4hm, and any unknown name.
proof idea
Definitional, not a proof. The body is nested string equality tests: if the input equals DS_1mode_10M, return accept; else if it equals Kerr_220_0M, accept; else if it equals Kerr_220_10M, accept; else reject. Downstream acceptance and rejection lemmas simply unfold this definition and simplify the equalities.
why it matters
This is the single policy object that all family-guard theorems in the module quote. Downstream results prove accept for the three mapped families and reject for Kerr 221 (plain and domega), MMRDNP, pseobnrv4hm, and unknown strings; eligible and blocked model counts also depend on it. It closes the runtime-policy side of the GWTC-3 ringdown verification stack without touching RS forcing (T0–T8), the Recognition Composition Law, or mass-ladder physics. The module doc stresses that the formalization is policy only: no likelihood is computed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.