dampingMedian
plain-language theorem explainer
Records the sample median of the per-cycle QNM damping ratio for the GWTC-3 one-member ringdown file rin_S190727h. Anyone comparing the RS echo-damping target 1/φ against that posterior cites this constant. It is a pure numeric definition, not a proved inequality.
Claim. The median of the derived one-member GWTC-3 ringdown damping-per-cycle statistic equals $0.845646710036$, where damping per cycle is $\exp(-1/(f_{t_0}\tau_{t_0}))$.
background
The module maps a single GWTC-3 ringdown HDF5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5) into a per-cycle quasi-normal-mode damping ratio. From the sampled frequency and damping time one forms
$$\mathrm{damping_per_cycle}=\exp\bigl(-1/(f_{t_0}\tau_{t_0})\bigr).$$
Recognition Science supplies a structural echo-damping target $1/\varphi\approx 0.618$, the Berry-scale reciprocal of the golden ratio forced at T6. Sibling constants in the same file give the mean, standard deviation, and the 5%, 16%, 84%, and 95% quantiles of that same derived posterior. The module status is structural theorem: zero sorry and no new RS axioms; the comparison is one-member only.
proof idea
No proof. The declaration is a def that pins a single real literal equal to the precomputed median of the mapped damping-per-cycle sample. Downstream residual and z-score defs read this constant (or the companion mean) by name.
why it matters
Gives the central tendency of the one-member damping posterior against which the RS target $1/\varphi$ is placed. The module doc states that the target already lies inside the central 68% and 90% intervals built from the sibling quantiles; the median anchors that interval comparison. It does not close an archive-wide claim, nor identify single-mode QNM damping per cycle with the full RS echo-train observable. It is bookkeeping for the first physically mapped GWTC-3 ringdown check in the verification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.