target_outside_90_interval
plain-language theorem explainer
The RS amplitude target log(φ^{-44}) lies strictly outside the central 90% posterior interval of log A_{t_0} for GWTC-3 ringdown member S190727h. Citation target for the one-member RS amplitude statistic certificate. Proof is a short contradiction: assume the target is in [q05,q95], then apply the prior strict inequality q95 < target and finish by linear arithmetic.
Claim. It is false that $q_{0.05}\le\log(\varphi^{-44})\le q_{0.95}$, where $q_{0.05}\approx-22.911$ and $q_{0.95}\approx-21.638$ are the empirical 5% and 95% quantiles of the posterior samples of $\log A_{t_0}$ for GWTC-3 ringdown member S190727h, and the RS structural target is $\log(\varphi^{-44})\approx-21.173$.
background
This module freezes a one-member comparison between Recognition Science's amplitude-scale target and a range-read GWTC-3 ringdown posterior. The member is rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, column logA_t_0. Status is structural theorem: zero sorry, zero new RS axioms.
The RS target is $\log(\varphi^{-44})\approx-21.173320302623$, the φ-ladder scale used as the structural amplitude reference. Empirical quantiles are numeric defs: 5th percentile $\approx-22.911$, 95th $\approx-21.638$. Posterior mean sits near $-22.245$ with std $\approx0.398$.
Upstream, target_above_q95 already proves $q_{0.95}<\log(\varphi^{-44})$ by unfolding the two numeric defs and norm_num. That strict inequality is the only nontrivial input to the present claim.
proof idea
Term-mode proof by contradiction. Introduce the assumption that the target lies in the closed interval between the 5th and 95th percentiles. Pull in the prior theorem that the 95th percentile is strictly less than the target. linarith discharges the resulting inconsistent pair of inequalities (target $\le q_{0.95}$ and $q_{0.95}<$ target). No further unfolding is needed.
why it matters
Packages into gwtc3RingdownOneMemberRSStatisticCert as the target_outside_90 field, alongside target-above-q95, outside-68%, and z-from-mean greater than two. That certificate is the first explicitly RS-referenced statistic on a range-read GWTC-3 ringdown posterior table.
In the broader framework the target $\log(\varphi^{-44})$ sits on the φ-ladder (φ forced at T6 as the self-similar fixed point). The result records that this scale sits above the bulk of this one-member amplitude posterior (about 2.69 std above the mean; sample fraction above target $\approx3.3\times10^{-4}$). It does not close an archive-wide likelihood or identify logA_t_0 as the final RS echo observable; those remain open verification steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.