damping_target_inside_90_interval
plain-language theorem explainer
The RS structural echo damping target 1/φ lies strictly inside the central 90% interval of the derived per-cycle QNM damping ratio for the GWTC-3 sample member rin_S190727h. Anyone citing the one-member ringdown damping comparison uses this inequality. The proof unfolds three frozen decimal constants and discharges both strict inequalities by norm_num.
Claim. The Recognition Science damping target $1/\varphi \approx 0.618034$ satisfies $q_{0.05} < 1/\varphi < q_{0.95}$, where $q_{0.05} = 0.279245$ and $q_{0.95} = 0.969863$ are the empirical 5th and 95th percentiles of the per-cycle damping statistic $\exp(-1/(f_{t_0}\tau_{t_0}))$ for the single GWTC-3 ringdown sample member.
background
This module records a one-member comparison of GWTC-3 ringdown quasi-normal-mode (QNM) damping against the Recognition Science structural echo target. From the sample HDF5 member, frequency $f_{t_0}$ and damping time $\tau_{t_0}$ are mapped to the per-cycle damping ratio $\exp(-1/(f_{t_0}\tau_{t_0}))$.
The RS target is $1/\varphi \approx 0.618033988750$, the reciprocal of the golden ratio forced at T6 of the forcing chain. The empirical quantiles $q_{0.05}$ and $q_{0.95}$ of that derived statistic are frozen as decimal constants in the module (0.279244551922 and 0.969863091765). The claim is that the target sits strictly between those two quantiles.
The setting is deliberately narrow: one range-read sample member only, not an archive-wide statement, and not an identification of single-mode QNM damping with the full RS echo-train observable.
proof idea
Numeric discharge only. Unfold the three definitions (5th percentile, RS target $1/\varphi$, 95th percentile) to their decimal literals, then apply norm_num to verify both strict inequalities on $\mathbb{R}$. No intermediate lemmas are required.
why it matters
Feeds the certificate gwtc3RingdownOneMemberDampingStatisticCert as the field target_inside_90, and appears as the first conjunct of the bundled one-statement theorem for the one-member damping statistic. Together with the 68% interval claim, the z-score bound, and the fraction-below-target validity check, it closes the structural verification that the RS damping target $1/\varphi$ is compatible with this GWTC-3 ringdown sample at the 90% level.
In the broader framework the target $1/\varphi$ is the structural echo damping scale tied to the golden ratio fixed at T6 (and the Berry creation threshold $\varphi^{-1}$). This lemma is a verification artifact, not a derivation of the target from first principles; it records that the forced constant lands inside the observational window for one mapped member.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.