dsFamilyModelName
plain-language theorem explainer
Names the controlled GWTC-3 ringdown family as the string DS_1mode_10M. Downstream family statistics and damping comparisons cite this label so every pooled figure is tied to one waveform-model semantics. The body is a literal string assignment.
Claim. The controlled-family model identifier is the string $\mathrm{DS\_1mode\_10M}$.
background
This module freezes a single controlled family from the GWTC-3 ringdown archive: model DS_1mode_10M, 22 HDF5 files, 22 events, and 643,624 pooled posterior samples. The observable is damping per cycle, $\mathrm{damping_per_cycle}=\exp(-1/(f_{t0}\tau_{t0}))$, compared to the Recognition Science target $1/\varphi\approx 0.618$.
The family is deliberately mono-model. It does not mix Kerr, MMRDNP, or other waveform semantics, and it is not a full-archive likelihood. Sibling definitions record pooled mean, std, median, and quantile bands for that same family; this string is the canonical name those records attach to.
proof idea
Definitional constant: the right-hand side is the string literal "DS_1mode_10M". No proof obligations, lemmas, or tactics.
why it matters
Gives a stable handle for the first controlled-family scaling of the Session 123 one-member QNM damping statistic. Recognition Science predicts a Berry-scale damping target near $1/\varphi$ (with $\varphi$ the golden ratio forced at T6). Tagging every pooled mean, interval containment count, and member-level check with this name keeps the verification mono-model and auditable. The module reports the RS target inside the pooled 68% and 90% bands; the name is what those claims are about.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.