ftauMean
plain-language theorem explainer
Records the sample mean of the ringdown product f τ for the single GWTC-3 member rin_S190727h (one-mode PyRing extract) as the real constant 9.950564161770. Downstream comparison theorems cite it against the RS fτ target. The body is a bare numeric definition, not a derived proof.
Claim. The mean product of ringdown frequency and damping time for the one-member GWTC-3 sample is the real number $9.950564161770$.
background
The module freezes a one-member GWTC-3 ringdown statistic. From the posterior samples of fundamental frequency $f_{t_0}$ and damping time $\tau_{t_0}$ one forms the per-cycle QNM damping ratio $\mathrm{damping_per_cycle}=\exp(-1/(f_{t_0}\tau_{t_0}))$. The Recognition Science structural echo-damping target is $1/\varphi\approx 0.618$.
The product $f\tau$ is the natural intermediate: larger $f\tau$ means weaker per-cycle damping. This declaration stores the sample mean of that product for the range-read HDF5 member rin/rin_S190727h_pyring_DS_1mode_10M.h5. Sibling constants hold the corresponding mean, std, median, and quantile summaries of the derived damping ratio itself.
Status is structural: zero sorry and no new RS-internal axioms. The comparison is deliberately one-member only.
proof idea
Pure definition: the real constant is written literally. No lemma applications, no tactics, no computation inside Lean beyond the numeral.
why it matters
Feeds the numeric inequality ftau_mean_gt_rs_target, which unfolds the RS $f\tau$ target and this mean and discharges the comparison by norm_num. That inequality, together with the damping-quantile containments, populates the certificate structure GWTC3RingdownOneMemberDampingStatisticCert (target inside the central 68% and 90% damping intervals, and $|z|<1$ from the damping mean).
In the broader RS verification layer this is the first physically mapped one-member ringdown damping check against the structural echo scale set by $\varphi^{-1}$. It does not yet identify single-mode QNM damping per cycle with the full RS echo-train observable; it only anchors the numeric sample mean used by those certificate fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.