logAQ84
plain-language theorem explainer
Numeric constant fixing the empirical 84% quantile of the GWTC-3 ringdown posterior on log-amplitude for member S190727h (column logA_t_0). Cited when checking whether the RS structural target log(φ^{-44}) lies inside the central 68% posterior interval. The body is a bare real literal read from the range-sampled HDF5 table; no proof obligations.
Claim. The empirical $84\%$ quantile of the posterior samples of $\log A_{t_0}$ for the GWTC-3 ringdown member is the real number $-21.824897151633$.
background
The module records a one-member amplitude-scale comparison between a range-read GWTC-3 ringdown posterior and a Recognition Science structural target. The member is rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, column logA_t_0.
The RS target is $\log(\varphi^{-44}) = -44\log\varphi \approx -21.173$. Sibling constants package the sample mean, std, median, and the $5%$, $16%$, $84%$, and $95%$ quantiles of that posterior. The $16%$ and $84%$ quantiles bound the central $68%$ interval used in the certificate.
This is pure data packaging: no RS-internal axiom and no claim that $\log A_{t_0}$ is the final echo-amplitude observable.
proof idea
Definition by numeric literal. The value is the precomputed empirical $84%$ quantile of the HDF5 posterior column; Lean stores it as a bare real constant with no tactic proof.
why it matters
Feeds the one-member certificate structure GWTC3RingdownOneMemberRSStatisticCert, whose field target_outside_68 asserts that the RS target is not between the $16%$ and $84%$ quantiles. The companion theorem target_outside_68_interval unfolds this constant together with the target and discharges the inequality by norm_num.
In the broader Verification domain this is the first explicitly RS-referenced statistic on a GWTC-3 ringdown table. It supports a negative placement claim only (target outside the central $68%$ and $90%$ bands, roughly $2.69\sigma$ above the mean). It does not close an archive-wide likelihood or identify the final RS echo amplitude observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.