logAQ95
plain-language theorem explainer
Numeric constant equal to the empirical 95% quantile of the GWTC-3 ringdown posterior on log amplitude for member S190727h (column logA_t_0). Cited by the one-member RS amplitude certificate and the theorems that place the RS target log(φ^{-44}) above this quantile and outside the central 90% interval. Pure data literal; no proof obligation.
Claim. Let $Q_{0.95}$ be the empirical $95\%$ quantile of the posterior samples of $\log A_{t_0}$ from the GWTC-3 ringdown HDF5 member $\mathrm{rin\_S190727h}$. Then $Q_{0.95} = -21.638354687882$.
background
The module freezes a single range-read GWTC-3 ringdown posterior (PyRing 1-mode, dataset /EXP6/posterior_samples, column logA_t_0) and compares it to the Recognition Science structural amplitude scale $\log(\varphi^{-44}) \approx -21.173$. Sibling constants record mean, std, median, and the $5%$, $16%$, $84%$, and $95%$ quantiles of that same posterior.
In RS units the golden ratio $\varphi$ is forced by the self-similarity fixed point (T6). The rung $-44$ target is the concrete scale against which this one-member amplitude posterior is scored. The module is explicitly one-member and amplitude-scale only: it does not identify logA_t_0 as the final echo observable and does not build an archive-wide likelihood.
proof idea
Definitional literal. The value is the precomputed empirical $95%$ quantile of the ingested posterior table; there is no tactic proof. Downstream theorems unfold the constant and discharge numeric comparisons by norm_num or linarith.
why it matters
Feeds the certificate structure GWTC3RingdownOneMemberRSStatisticCert via the fields target_above_q95 and target_outside_90, and appears in the one-statement theorem that packages the whole one-member statistic (target above Q95, $z$-score from the mean above 2, sample fraction above target below $0.001$).
Together with the matching lower quantile, it is the concrete bound that places $\log(\varphi^{-44})$ outside the central $90%$ posterior interval for this member. That is the first explicitly RS-referenced amplitude-scale comparison on a real GWTC-3 ringdown table in the verification layer. It does not close an archive-wide claim; it only pins the numeric edge used by the local certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.