logAQ05
plain-language theorem explainer
Numeric constant fixing the 5% 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 90% credible interval. The value is a hard-coded sample summary, not a derived identity.
Claim. The empirical $5\%$ quantile of the posterior samples of $\log A_{t_0}$ for the GWTC-3 ringdown member S190727h equals $-22.911300360855$.
background
This 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 reference scale is $\log(\varphi^{-44}) = -44\log\varphi \approx -21.173320302623$. Sibling constants in the same file pin the posterior mean, std, median, and the $16%$, $84%$, and $95%$ quantiles of the same sample. Together they support interval-membership checks against the target.
The setting is verification only: one event, one column, no archive-wide likelihood and no claim that $\log A_{t_0}$ is the final RS echo amplitude observable.
proof idea
Definitional constant: the real literal is the precomputed $5%$ sample quantile from the HDF5 posterior table. No tactic proof and no lemma application; downstream theorems treat the value as a fixed real.
why it matters
Feeds the certificate structure GWTC3RingdownOneMemberRSStatisticCert and the theorem target_outside_90_interval, which assert that the RS target is not inside the central $90%$ posterior interval (equivalently, not between this $5%$ quantile and the $95%$ quantile). That is the first explicitly RS-referenced statistic on a range-read GWTC-3 ringdown table in the monolith.
In the broader framework the target $\log(\varphi^{-44})$ sits on the $\varphi$-ladder used for mass and amplitude scales; the comparison is a structural consistency check, not a derivation of $\varphi$ or of the eight-tick octave. It closes a verification stub for this single member while leaving open whether the same column is the correct RS echo amplitude across the full GWTC-3 archive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.