dampingZFromMean
plain-language theorem explainer
Numeric constant equal to the z-score of the RS echo-damping target against the posterior mean of one GWTC-3 ringdown member's per-cycle damping. Anyone citing the one-member damping certificate or the bundled one-statement theorem needs this value. It is a bare real literal, not a derived computation in Lean.
Claim. The standardized residual of the Recognition Science per-cycle damping target from the sample mean of the one-member GWTC-3 ringdown damping posterior is the real number $0.665820924556$.
background
The module records a single GWTC-3 ringdown HDF5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5). Frequency and damping time of the fundamental QNM are mapped to the per-cycle damping ratio $\mathrm{damping_per_cycle} = \exp(-1/(f_{t_0}\tau_{t_0}))$.
Recognition Science predicts a structural echo-train damping target of $1/\varphi \approx 0.618034$. Sibling constants in the module fix the posterior mean, standard deviation, median, and quantile ladder of that derived damping statistic for the one member.
This declaration is the z-score of the RS target relative to that posterior mean (residual divided by the sample standard deviation). The module status is structural: zero sorry, no new RS axioms, and explicitly one-member only.
proof idea
Definition by numeric literal. The body is the concrete real $0.665820924556$ with no further Lean computation. Downstream theorems simply unfold the name and discharge inequalities by norm_num.
why it matters
Feeds three local consumers: the inequality dampingZFromMean < 1, the certificate structure field z_lt_one, and the bundled one-statement theorem that packages target-inside-90%, target-inside-68%, and $z<1$ together with non-emptiness of the cert.
In the Recognition framework this is empirical verification scaffolding, not a forcing-chain step. It checks that the RS damping target $1/\varphi$ (the Berry-scale reciprocal of the golden ratio fixed at T6) sits well inside one standard deviation of a real LIGO/Virgo ringdown posterior. The module itself warns that this does not identify single-mode QNM damping with the final RS echo-train observable, and it is not archive-wide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.