dampingResidualFromMean
plain-language theorem explainer
Numeric residual of the one-member GWTC-3 ringdown damping-per-cycle sample mean from the RS structural target $1/\varphi$. Verification authors cite it when placing the sample mean relative to the echo-damping benchmark. It is a frozen real literal, not a proved identity.
Claim. The residual of the one-member GWTC-3 derived damping-per-cycle mean from the Recognition Science structural target $1/\varphi$ is the fixed real $0.146557727857$.
background
This module records a one-member GWTC-3 ringdown comparison. From the posterior sample of a single event file (rin/rin_S190727h_pyring_DS_1mode_10M.h5), the frequencies $f_{t_0}$ and damping times $\tau_{t_0}$ are mapped to the per-cycle QNM damping ratio
$$\mathrm{damping_per_cycle}=\exp\bigl(-1/(f_{t_0}\tau_{t_0})\bigr).$$
The RS structural echo-damping target is $1/\varphi\approx 0.618034$. Sibling constants in the same file freeze the sample mean, standard deviation, median, and quantile cuts of that derived damping statistic, plus the target itself.
The residual named here is the signed (or absolute) offset of that sample mean from the RS target. The module status is structural: zero sorry, zero new RS axioms; it is explicitly not an archive-wide claim.
proof idea
No proof. The declaration is a bare def equal to the decimal literal 0.146557727857. The value is the precomputed residual of the sample damping mean from the RS target, recorded for downstream numeric comparison rather than derived inside Lean.
why it matters
It anchors the one-member damping comparison that the module advertises: the RS target $1/\varphi$ sits inside the central 68% and 90% intervals of the derived damping statistic for this GWTC-3 ringdown member. Together with the sibling mean, std, and quantile constants, it lets later verification lemmas state how far the sample mean sits from the structural echo-damping benchmark without re-reading HDF5.
In the broader RS picture the target $1/\varphi$ is the Berry-scale / golden-ratio damping level tied to the self-similar fixed point $\varphi$ (forcing chain T5–T6). This residual does not identify single-mode QNM damping per cycle with the final RS echo-train observable; it only freezes the numeric gap for this one mapped member.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.