z_from_mean_gt_two
plain-language theorem explainer
The standardized residual of the GWTC-3 ringdown log-amplitude posterior mean against the RS target log(φ^{-44}) is strictly larger than 2. Citation target for anyone packaging the one-member ringdown amplitude-scale certificate. Proof is a two-step term discharge: unfold the recorded z constant, then norm_num.
Claim. Let $z_{\mathrm{mean}} = 2.689626$ be the recorded standardized residual of the RS target $\log(\varphi^{-44})$ relative to the posterior mean of $\log A_{t_0}$ (in units of the posterior standard deviation). Then $2 < z_{\mathrm{mean}}$.
background
This module freezes a single GWTC-3 ringdown posterior member (rin_S190727h, dataset /EXP6/posterior_samples, column logA_t_0) against the RS structural amplitude target $\log(\varphi^{-44}) \approx -21.173$. Reported summary numbers include posterior mean $\approx -22.245$, std $\approx 0.398$, and the standardized residual of the target above the mean $\approx 2.690$.
The local definition logAZFromMean is the literal real constant $2.689626$ standing for that residual (target minus mean, divided by std). Sibling constants record the mean, std, median, quantile edges, and the sample fraction above target. The module is a structural verification artifact only: one-member amplitude-scale comparison, not an archive-wide likelihood.
Upstream, the inequality depends solely on that constant definition; no further analytic lemma is required.
proof idea
Term-mode, two tactics. Unfold the definition of the z-from-mean constant to the literal real $2.689626$, then apply norm_num to discharge $2 < 2.689626$. No external lemmas beyond the definition itself.
why it matters
Feeds the certificate record gwtc3RingdownOneMemberRSStatisticCert as the field z_gt_two, and appears as the middle conjunct of the one-statement theorem gwtc3_ringdown_one_member_rs_statistic_one_statement (together with target above Q95, fraction above target below $0.001$, and nonemptiness of the cert). That package is the first explicitly RS-referenced statistic on a range-read GWTC-3 ringdown posterior table, closed with zero sorry and zero new RS axioms.
In the broader Recognition framework this is verification scaffolding, not a forcing-chain step: it checks that the $\varphi$-ladder amplitude target $\log(\varphi^{-44})$ sits more than two posterior standard deviations above the mean of this one event's logA_t_0 samples. It does not settle whether logA_t_0 is the final RS echo amplitude observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.