target_outside_68_interval
plain-language theorem explainer
The RS structural target log(φ^{-44}) lies strictly outside the central 68% posterior interval of logA_t_0 for the GWTC-3 ringdown member S190727h. Anyone citing the one-member RS amplitude statistic uses this as the 68% exclusion half of the certificate. The proof is a short numeric contradiction: unfold the Q84 and target constants and discharge with norm_num.
Claim. It is not the case that $\log(\varphi^{-44})$ lies in the closed central 68\% posterior interval of $\log A_{t_0}$ for the S190727h ringdown sample: $\neg\bigl(q_{16}(\log A_{t_0}) \le \log(\varphi^{-44}) \le q_{84}(\log A_{t_0})\bigr)$, with $q_{16}\approx -22.720$, $q_{84}\approx -21.825$, and $\log(\varphi^{-44})\approx -21.173$.
background
This module is a structural verification theorem for one GWTC-3 ringdown posterior: member rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, column logA_t_0. The RS structural amplitude target is $\log(\varphi^{-44})=-44\log\varphi\approx -21.173320302623$, recorded as a concrete real constant.
The posterior quantiles used here are frozen sample summaries: the 16th percentile $q_{16}\approx -22.7198$ and the 84th percentile $q_{84}\approx -21.8249$. Together they form the usual central 68% credible interval for a unimodal posterior. The module also records mean, median, 90% quantiles, residual $z$-score, and fraction above target; this declaration isolates only the 68% membership claim.
The setting is deliberately one-member and amplitude-scale only. It does not identify $\log A_{t_0}$ as the final RS echo observable, and it does not aggregate an archive-wide likelihood.
proof idea
Assume for contradiction that the target sits between the 16th and 84th percentiles. Unfold the concrete definitions of $q_{84}$ and of the RS target $\log(\varphi^{-44})$ in the hypothesis. The resulting numeric conjunction is false by norm_num (the target is larger than $q_{84}$), so the assumption is impossible. The 16th percentile is not needed once the upper bound already fails.
why it matters
This is one of the four boolean fields packed into gwtc3RingdownOneMemberRSStatisticCert, the module's certificate object: target above $q_{95}$, outside the 90% interval, outside the 68% interval, and $z>2$ from the mean. Together they turn the range-read HDF5 summary into a machine-checkable RS-referenced statistic with zero sorry and no new RS axioms.
In the Recognition framework the target $\log(\varphi^{-44})$ is a pure $\varphi$-ladder amplitude scale (rung offset 44 on the log-phi ladder). The certificate records that, for this single ringdown member, that scale sits well above the bulk of the posterior. Downstream consumers can cite the cert rather than re-deriving the numeric comparisons. The module itself flags the open question: this is not yet an archive-wide likelihood, nor a proof that $\log A_{t_0}$ is the definitive RS echo amplitude observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.