logAZFromMean
plain-language theorem explainer
Numeric constant fixing the z-score of the RS amplitude target log(φ^{-44}) above the GWTC-3 ringdown posterior mean of log A for event S190727h: about 2.69 standard deviations. Verification authors cite it when stating that the target sits more than two σ above the mean. It is a bare real definition, not an inequality proof.
Claim. Define the mean-based z-score $z_{\mathrm{mean}} := 2.689626$, equal to the number of posterior standard deviations by which the RS structural target $\log(\varphi^{-44})\approx -21.17332$ lies above the sample mean of $\log A_{t_0}$ on the GWTC-3 ringdown posterior for member S190727h.
background
This module records a one-member Recognition Science amplitude-scale comparison against a range-read GWTC-3 ringdown posterior (HDF5 member rin_S190727h, dataset /EXP6/posterior_samples, column logA_t_0). The RS structural target is $\log(\varphi^{-44})=-44\log\varphi\approx -21.173320302623$.
Sibling constants pin the sample summary: posterior mean $\approx -22.244585483768$, std $\approx 0.398295292686$, median and central quantiles likewise. The z-score is the standardized residual (target minus mean) divided by the posterior std, precomputed offline and frozen here as a real literal.
The module is a structural verification certificate only: zero sorry, no new RS axioms. It does not identify $\log A_{t_0}$ as the final RS echo amplitude observable, nor does it run an archive-wide likelihood.
proof idea
Pure numeric definition: the real literal $2.689626$ is assigned directly. No tactics, no lemmas. Downstream inequalities such as $2 < z_{\mathrm{mean}}$ discharge by unfold plus norm_num on this constant.
why it matters
Feeds the one-member RS amplitude statistic package. The theorem z_from_mean_gt_two proves $2 < z_{\mathrm{mean}}$ by unfolding this constant. The one-statement theorem conjoins that fact with target-above-Q95, fraction-above-target $< 0.001$, and nonemptiness of the certificate structure whose fields record that the target lies outside the central 68% and 90% posterior intervals.
In the broader RS verification layer this is the first explicitly RS-referenced statistic on a GWTC-3 ringdown posterior table, tying the $\varphi$-ladder amplitude scale (here rung-like exponent $-44$) to LIGO/Virgo ringdown posteriors. It is deliberately one-member and amplitude-scale only; archive-wide or multi-mode closure remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.