dsMembersInside68Count
plain-language theorem explainer
Records that 13 of the 22 GWTC-3 ringdown members in the controlled DS_1mode_10M family have the RS damping target 1/φ inside their member-level central 68% interval. Citation target for family hit-rate comparisons and the DS master certificate. Pure numeric definition; no proof obligation.
Claim. In the controlled GWTC-3 ringdown family with model $\mathrm{DS\_1mode\_10M}$ (22 members), the number of members whose central $68\%$ credible interval for damping-per-cycle contains the RS target $1/\varphi$ is $13$.
background
The module freezes a controlled-family scaling of the one-member QNM damping statistic on GWTC-3. Family semantics are fixed: model DS_1mode_10M, 22 HDF5 files, 22 events, and 643624 pooled posterior samples. The observable is damping per cycle, $\exp(-1/(f_{t_0}\tau_{t_0}))$, with RS target $1/\varphi\approx 0.618$.
Sibling constants record the pooled posterior (mean $\approx 0.581$, std $\approx 0.265$, median $\approx 0.570$, and the $16/84$ and $5/95$ quantiles). The module states that the target lies inside both the pooled $90%$ and $68%$ intervals, and that 13 of 22 member-level $68%$ intervals contain the target. This definition is that integer hit count.
It is controlled-family only: no mixing of Kerr, MMRDNP, or other waveform-model semantics, and not a full-archive likelihood.
proof idea
Definitional constant: the natural number $13$ is assigned directly. No tactics, lemmas, or computation run at this site. Downstream theorems unfold the name and discharge inequalities by decide.
why it matters
Supplies the DS-family member hit count used by the nonzero-bounds theorem ($0 < 13 < 22$), the DS family master certificate structure, and the cross-family comparison layer. In particular, hit_count_order ranks the three controlled families by $68%$ hit count and places this DS count strictly above the two Kerr families; the one-statement comparison theorem aggregates those ranks with pooled-mean orderings.
Within Recognition Science verification, the target $1/\varphi$ is the Berry-scale reciprocal fixed by the forcing chain (T6 $\varphi$ as self-similar fixed point). A high member-level containment rate in a single, taxonomy-clean damped-sinusoid family is structural evidence that the RS damping anchor is not an artifact of pooling alone. The module is marked structural closure (zero sorry, zero new RS axioms).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.