dsPooledQ95
plain-language theorem explainer
Records the pooled 95th percentile of the damping-per-cycle posterior for the GWTC-3 DS_1mode_10M ringdown family as the real constant 0.958639185642. Anyone checking that the RS target 1/φ sits inside the family's central 90% interval cites this bound. It is a bare numeric definition, not a derived lemma.
Claim. The pooled 95th percentile of the GWTC-3 ringdown family observable $\mathrm{damping\_per\_cycle}=\exp(-1/(f_{t_0}\tau_{t_0}))$ over the $DS\_1mode\_10M$ controlled family (22 events, 643624 posterior samples) equals $0.958639185642$.
background
The module freezes a controlled-family scaling of the Session 123 one-member QNM damping statistic. The family is 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}))$.
The Recognition Science target for this observable is $1/\varphi\approx 0.618034$. Sibling constants record the pooled mean, std, median, and the q05/q16/q84/q95 quantiles of the same pooled posterior. This declaration is the upper edge of the central 90% interval (paired with the pooled 5th percentile).
The module is structural only: it does not mix Kerr, MMRDNP, or other waveform-model semantics, and it is not a full archive likelihood. Status is zero sorry and zero new RS-specific axioms.
proof idea
Bare definition: the real constant is assigned the decimal value 0.958639185642 with no proof obligations. Downstream theorems unfold the name and discharge numeric comparisons by norm_num.
why it matters
Supplies the upper endpoint for the pooled 90% containment check. The theorem ds_target_inside_pooled_90 asserts that the RS damping target lies strictly between the pooled 5th and 95th percentiles; its proof unfolds this constant and finishes by norm_num.
The same bound is a field obligation of the family certificate structure and appears in the one-statement controlled-family damping theorem, which packages member count, event count, sample count, and both the 90% and 68% target-containment facts. In the broader RS verification stack this is empirical support that $1/\varphi$ (the Berry-scale inverse golden ratio) sits inside the observed ringdown damping distribution for a single, homogeneous model family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.