guard_accepts_DS
plain-language theorem explainer
The GWTC-3 ringdown runtime family guard accepts the DS one-mode 10M model string. Verification authors cite this when assembling the family-guard certificate or the one-statement guard theorem. The proof is a two-step unfold-and-simp against the hardcoded decision table.
Claim. Evaluating the ringdown family guard on the model label $\mathrm{DS\_1mode\_10M}$ yields the accept decision.
background
The module formalizes a runtime policy induced by the Session 131 family-stratified likelihood selector for GWTC-3 ringdown analyses. It does not compute posteriors; it only records which model-family strings are eligible.
The decision function maps a model string to accept or reject. By definition it accepts exactly three labels: DS one-mode 10M, Kerr 220 at 0M, and Kerr 220 at 10M; every other string, including Kerr 221 variants, MMRDNP, pseobnrv4hm, and unknowns, is rejected.
This lemma is the first accept clause of that table: the DS one-mode 10M family is on the allow-list.
proof idea
Unfold the decision function, then simplify. The first branch of the if-chain matches the string $\mathrm{DS_1mode_10M}$ and returns accept, so simp closes the equality. No external lemmas are required.
why it matters
This is one of the three positive accept facts packed into the family-guard certificate and into the one-statement runtime guard theorem (conjunction of three accepts and several rejects). Downstream, the guarded-family-scripts module reuses it as guarded_DS_script_accepted and folds it into the scripts one-statement theorem that also records smoke-test counts.
In the Recognition verification layer this is structural policy closure, not a physics derivation: it pins which ringdown model families may enter later likelihood or certificate pipelines. It sits beside the sibling accept facts for the two Kerr-220 families and the reject facts for blocked families. Zero sorry, zero new RS axioms; status is full structural theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.