guarded_DS_script_accepted
plain-language theorem explainer
The DS one-mode 10M ringdown family string is accepted by the runtime family guard. Anyone wiring GWTC-3 ringdown family scripts to the eligibility gate cites this. The proof is a one-line wrapper of the corresponding guard lemma.
Claim. The runtime family guard returns accept on the model identifier $\mathrm{DS\_1mode\_10M}$.
background
Session 133 wires a runtime family guard into the mapped GWTC-3 ringdown family-statistic scripts. Before any script reads posterior data it must call an eligibility check on its model name. The guard is a pure string decision: three named families are accepted and every other string is rejected.
The accepted set is exactly the three patched scripts: the DS one-mode 10M damping family, the Kerr 220 0M damping family, and the Kerr 220 10M damping family. This module records only operational guarding; it adds no new physics mapping and computes no new likelihood.
Upstream, guardModel is the decision table and guard_accepts_DS already proves the DS entry evaluates to accept by unfolding and simplifying that table.
proof idea
One-line wrapper that applies guard_accepts_DS. That upstream lemma unfolds the guard decision table and simplifies the DS branch to accept; this theorem simply re-exports the same equality under the guarded-scripts module name.
why it matters
Feeds the certificate bundle gwtc3RingdownGuardedFamilyScriptsCert, which packages guarded-script count, smoke-test passage, and per-family acceptance facts. The DS acceptance field of that cert is filled by this theorem.
In the Recognition verification layer this is structural closure for Session 133: eligible mapped families pass the gate, while blocked or unknown names fail. It does not touch the forcing chain (T0–T8), the Recognition Composition Law, or mass/ladder physics; it only locks the operational allow-list used by the GWTC-3 ringdown family scripts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.