logAPosteriorStd
plain-language theorem explainer
Records the sample standard deviation of the GWTC-3 ringdown posterior column logA_t_0 for event S190727h as the fixed real 0.398295292686. Citation target for one-member RS amplitude-scale checks against log(φ^{-44}). Pure numeric definition from the range-read HDF5 posterior table; no proof obligations.
Claim. The posterior standard deviation of the ringdown amplitude column $\log A_{t_0}$ for GWTC-3 member S190727h (PyRing DS, 1-mode, $10M$ samples) is the constant $\sigma(\log A_{t_0}) = 0.398295292686$.
background
The module freezes a single GWTC-3 ringdown posterior for RS amplitude comparison. Member file rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, column logA_t_0. Recognition Science supplies the structural target $\log(\varphi^{-44}) = -44\log\varphi \approx -21.173320302623$ on the $\varphi$-ladder (mass/amplitude rungs).
Sibling constants in the same file pin the rest of the one-member summary: posterior mean $\approx -22.2446$, median $\approx -22.2119$, and quantile edges used to show the target lies outside the central 68% and 90% intervals. The std here is the scale against which the residual from the mean is measured (about $2.69\sigma$).
Status is structural recording only: zero sorry, zero new RS axioms. It does not assert that $\log A_{t_0}$ is the definitive RS echo observable.
proof idea
Definitional constant: the real literal $0.398295292686$ is assigned directly as the precomputed posterior standard deviation from the range-read HDF5 sample summary. No tactics, no lemmas, no algebraic reduction.
why it matters
Gives the denominator for the one-member $z$-score of the RS target $\log(\varphi^{-44})$ relative to the S190727h ringdown posterior mean. Downstream siblings (logAZFromMean, residual and fraction-above-target defs) use this scale to report that the target sits roughly $2.69$ posterior std above the mean and that only a $3.31\times 10^{-4}$ sample fraction exceeds it.
In the Recognition verification layer this is the first explicitly RS-referenced amplitude statistic on a GWTC-3 ringdown table. It supports structural comparison only; it does not close an archive-wide likelihood or identify $\log A_{t_0}$ as the final echo amplitude observable. Landmark contact is the $\varphi$-ladder rung structure (target $\varphi^{-44}$), not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.