damping_target_inside_68_interval
plain-language theorem explainer
The RS echo-damping target 1/φ lies strictly inside the central 68% interval of the derived per-cycle damping posterior for the single GWTC-3 ringdown sample member. Verification authors cite it when assembling the one-member damping certificate. The proof unfolds the three numeric defs and discharges the two inequalities by norm_num.
Claim. For the range-read GWTC-3 ringdown sample member, the Recognition Science structural damping target $1/\varphi \approx 0.618034$ satisfies $q_{16} < 1/\varphi < q_{84}$, where $q_{16}$ and $q_{84}$ are the 16th and 84th percentiles of the derived per-cycle QNM damping ratio $\mathrm{damping\_per\_cycle} = \exp(-1/(f_{t_0}\tau_{t_0}))$.
background
This module records a one-member GWTC-3 ringdown comparison. From the sample HDF5 member rin/rin_S190727h_pyring_DS_1mode_10M.h5, the ringdown frequency and damping time $(f_{t_0},\tau_{t_0})$ are mapped to the per-cycle QNM damping ratio $\mathrm{damping_per_cycle}=\exp(-1/(f_{t_0}\tau_{t_0}))$. Posterior quantiles of that derived statistic are frozen as concrete reals.
The RS structural echo-damping target is $1/\varphi\approx 0.618033988750$ (the reciprocal of the golden ratio fixed by the T6 self-similar fixed point; also the Berry creation threshold $\varphi^{-1}$). The three constants used here are rsDampingTarget $=0.618033988750$, dampingQ16 $=0.552717258546$, and dampingQ84 $=0.950497542361$.
The local claim is only that the target sits inside the central 68% interval of this one sample member. It is not an archive-wide statement and does not identify single-mode QNM damping per cycle with the final RS echo-train damping observable.
proof idea
Term-mode proof by unfolding the three numeric definitions and applying norm_num. After unfold, the goal is the concrete pair of real inequalities $0.552717258546 < 0.618033988750$ and $0.618033988750 < 0.950497542361$, both discharged by decimal arithmetic. No lemmas beyond the three local defs are required.
why it matters
Feeds the certificate bundle gwtc3RingdownOneMemberDampingStatisticCert as the target_inside_68 field, and appears as the second conjunct of the one-statement theorem gwtc3_ringdown_one_member_damping_statistic_one_statement. Together with the matching 90% interval, mean-z, and fraction checks, it closes the structural (0-sorry, 0 new RS axiom) one-member damping comparison recorded in this module.
In the Recognition framework the target $1/\varphi$ is the Berry creation threshold and the structural echo-damping scale on the phi ladder. Landing it inside the observed 68% band for even a single mapped GWTC-3 ringdown member is the first physically mapped check of that scale against LIGO/Virgo ringdown posteriors. The module status line marks closure 2026-05-22; the remaining open question is archive-wide aggregation and whether single-mode QNM damping per cycle equals the final RS echo-train observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.