dampingFractionBelowTarget
plain-language theorem explainer
Numeric constant fixing the empirical fraction of the one-member GWTC-3 ringdown damping posterior that lies below the RS echo target 1/φ at about 0.208. GWTC-3 verification and certificate constructions cite it when placing the target inside sample quantiles. The body is a bare real literal, not a derived identity.
Claim. The empirical fraction of the one-member GWTC-3 ringdown per-cycle damping posterior lying below the Recognition Science target $1/\varphi$ is the fixed real $0.208416038110$.
background
This module records a one-member GWTC-3 ringdown comparison. Observed 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}))$. The RS structural echo-damping target is $1/\varphi\approx 0.618$.
Sibling constants in the same file hold the sample mean, standard deviation, median, and the 5/16/84/95 percent quantiles of that derived damping statistic for the range-read member rin/rin_S190727h_pyring_DS_1mode_10M.h5. The present definition is the complementary empirical mass below the RS target.
The module is structural verification only: zero sorry, no new RS axioms, and explicitly not an archive-wide claim.
proof idea
Definition by numeric literal. There is no tactic proof and no lemma application; the value is the precomputed posterior fraction written as a ℝ constant. Downstream theorems simply unfold this name and discharge inequalities by norm_num.
why it matters
Supplies the mass-below-target figure used by the one-member damping certificate. The sibling theorem damping_fraction_below_target_between_zero_and_one proves the constant lies in $(0,1)$. The certificate structure GWTC3RingdownOneMemberDampingStatisticCert packages the stronger placement facts that the RS target sits inside the central 68% and 90% intervals and that the standardized residual from the mean is less than one.
In the broader RS picture the target $1/\varphi$ is the Berry-scale / golden-ratio damping level tied to the forcing chain (φ as self-similar fixed point). This constant is the first physically mapped one-member check that a real GWTC-3 ringdown posterior puts non-trivial mass both below and above that level, without claiming identity between single-mode QNM damping and the full RS echo-train observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.