logAQ16
plain-language theorem explainer
Numeric constant fixing the 16th percentile of the GWTC-3 S190727h ringdown posterior for log-amplitude at about -22.720. Cited when testing whether the RS structural target log(φ^{-44}) sits inside the central 68% credible interval. Pure data-backed definition with no proof obligations.
Claim. The lower edge of the central 68% posterior interval for the ringdown log-amplitude $\log A_{t_0}$ on GWTC-3 member S190727h is fixed as $Q_{16}(\log A_{t_0}) = -22.719806844144$.
background
This module records a one-member RS amplitude comparison against a range-read GWTC-3 ringdown posterior (file rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, column logA_t_0). The RS structural target is $\log(\varphi^{-44}) = -44\log\varphi \approx -21.173$.
Sibling constants encode the usual posterior summaries: mean, std, median, and the 5/16/84/95 percent quantiles of $\log A_{t_0}$. The 16th and 84th percentiles bound the central 68% credible interval used in standard GW parameter estimation.
The comparison is amplitude-scale only. It does not identify $\log A_{t_0}$ as the final RS echo observable, nor does it form an archive-wide likelihood.
proof idea
Definitional constant: the real literal $-22.719806844144$ is assigned directly. No tactics, lemmas, or algebraic reduction. Downstream theorems unfold the name and discharge interval claims by norm_num.
why it matters
Supplies the lower endpoint for the 68% interval test. The theorem target_outside_68_interval proves $\neg(Q_{16} \le \log(\varphi^{-44}) \le Q_{84})$ by unfolding this constant against the RS target and reducing numerically. The certificate structure GWTC3RingdownOneMemberRSStatisticCert packages that fact with the matching 90% exclusion and the stricter $Q_{95}$ bound.
In the Recognition framework this is empirical verification scaffolding: a single-event check that the forced $\varphi$-ladder amplitude $\varphi^{-44}$ lies well above the observed ringdown posterior mass (about 2.69 posterior std above the mean; sample fraction above target $\approx 3.3\times 10^{-4}$). It does not close an archive-wide claim; it pins one concrete quantile so the structural certificate can be stated without external data axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.