rsFtauTarget
plain-language theorem explainer
Numeric RS target for the ringdown product f τ, equal to 1/ln(φ) ≈ 2.078086921235, so that exp(−1/(fτ)) recovers the structural echo damping 1/φ. Used by the one-member GWTC-3 damping comparison and its certificate. Defined by a fixed real literal; no proof obligations.
Claim. The Recognition Science target value of the ringdown frequency–damping product is $f\tau = 2.078086921235$ (equivalently $1/\ln\varphi$), the unique positive real such that $\exp(-1/(f\tau)) = 1/\varphi$.
background
This module records a one-member GWTC-3 ringdown statistic. Observed mode frequency $f_{t_0}$ and damping time $\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$. Inverting that relation gives the product target $f\tau = 1/\ln\varphi$, which is the constant defined here. Sibling constants package the sample mean, quantiles, and residual of the derived damping statistic for the range-read member rin/rin_S190727h_pyring_DS_1mode_10M.h5.
The module is a structural verification layer (zero sorry, no new RS axioms). It compares one sample member only; it does not identify single-mode QNM damping with the full RS echo-train observable.
proof idea
Definition by a single real literal. No tactics, lemmas, or algebraic reduction: the value $2.078086921235$ is hard-coded as the decimal expansion of $1/\ln\varphi$ used by the downstream numeric comparisons.
why it matters
Anchors the product-side half of the one-member damping check. Downstream, ftau_mean_gt_rs_target proves the sample mean product strictly exceeds this target by norm_num after unfolding. The certificate structure GWTC3RingdownOneMemberDampingStatisticCert packages the companion damping-side claims (target inside the central 68% and 90% intervals, $|z|<1$ from the mean).
In the RS framework the damping floor $1/\varphi$ is the Berry creation threshold (primer). Fixing $f\tau = 1/\ln\varphi$ is the unique product that realizes that floor under the exponential map used for per-cycle QNM damping. The result is verification scaffolding for GWTC-3 ringdown, not a derivation of $\varphi$ itself (that sits in the T5–T6 forcing chain).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.