dsPooledStd
plain-language theorem explainer
Records the pooled posterior standard deviation 0.264599094550 of the damping-per-cycle observable over the controlled GWTC-3 family DS_1mode_10M (22 events, 643624 samples). Anyone citing the family-level ringdown damping comparison against the RS target 1/φ needs this width. It is a literal real constant, not a derived proof.
Claim. The pooled standard deviation of the damping-per-cycle posterior samples for the GWTC-3 ringdown family with model $\mathrm{DS\_1mode\_10M}$ equals $0.264599094550$.
background
The module freezes a controlled-family scaling of the one-member QNM damping statistic on GWTC-3 ringdown posteriors. The family is fixed to model DS_1mode_10M: 22 HDF5 files, 22 events, and 643624 pooled posterior samples. No Kerr, MMRDNP, or other waveform-model semantics are mixed in.
The observable is damping per cycle, $\mathrm{damping_per_cycle}=\exp(-1/(f_{t0}\tau_{t0}))$. Recognition Science predicts a target near the golden-ratio reciprocal $1/\varphi\approx 0.618034$. Sibling constants in the same module record the pooled mean, median, and quantile envelope of that same pooled sample cloud; this declaration is the pooled standard deviation of that cloud.
proof idea
No proof. The declaration is a definitional binding of a single real literal computed offline from the pooled posterior samples and written into Lean as 0.264599094550.
why it matters
Family-level width is what lets the module claim that the RS target $1/\varphi$ sits inside the pooled 68% and 90% intervals and that 13 of 22 member-level 68% intervals contain the target. Without a recorded pooled std, those interval statements have no numeric anchor.
In the broader RS picture the target $1/\varphi$ is the Berry creation threshold from the forcing chain (T6 $\varphi$ fixed point). This constant is verification infrastructure only: it documents an external GW archive statistic against that threshold. It does not derive $\varphi$, the eight-tick structure, or any mass-ladder rung; it only freezes the empirical scatter used by the structural closure of this controlled-family check (zero sorry, zero new RS axioms).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.