gwtc3RingdownOneMemberRSStatisticCert
plain-language theorem explainer
Packages the one-member GWTC-3 ringdown amplitude comparison against the RS structural target log(φ^{-44}) into a single certificate record. Anyone citing the first explicit RS-referenced statistic on a range-read GWTC-3 ringdown posterior would point here. Construction is a pure structure inhabitant: six already-proved numerical facts plus the nonempty posterior-summary witness are wired field-by-field.
Claim. There is a certificate asserting: the RS target $\log(\varphi^{-44})$ lies strictly above the 95th percentile of the $\log A_{t_0}$ posterior; it lies outside both the central 90% and central 68% posterior intervals; its $z$-score from the posterior mean exceeds 2; the sample fraction above the target is strictly less than $0.001$; and a nonempty GWTC-3 ringdown HDF5 posterior-summary certificate is available.
background
This module records a one-member amplitude-scale comparison on a range-read GWTC-3 ringdown posterior. The member is rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, column logA_t_0. The RS structural target is $\log(\varphi^{-44}) = -44\log\varphi \approx -21.173$.
Reported posterior numbers: mean $\approx -22.245$, std $\approx 0.398$, median $\approx -22.212$. The target sits about $2.69$ posterior std above the mean; the sample fraction above target is $0.000331$. Sibling constants fix the quantiles ($q_{05}, q_{16}, q_{84}, q_{95}$), residual and $z$ from the mean, and the fraction above target.
The certificate structure bundles six props: target above $q_{95}$; outside the 90% and 68% central intervals; $z>2$; fraction $<0.001$; and nonempty summary cert from the imported HDF5 sample-summary module. Status is structural (zero sorry, zero new RS axioms).
proof idea
One-line structure inhabitant. Each field is filled by a named sibling theorem already closed by norm_num (or a one-line reduction to such):
target_above_q95unfolds the $q_{95}$ and target constants and closes bynorm_num.target_outside_90_intervalintroduces the conjunction, reuses the $q_{95}$ inequality, and finishes bylinarith.target_outside_68_intervalintroduces the conjunction and closes bynorm_numon the unfolded bounds.z_from_mean_gt_twoandfraction_above_target_smallare directnorm_numfacts on the residual/$z$ and fraction constants.posterior_summary_availableis the inhabited witness of the imported HDF5 summary cert.
No new arithmetic is done at this site.
why it matters
This is the master certificate object for the first explicitly RS-referenced statistic on a GWTC-3 ringdown posterior table. Downstream, gwtc3RingdownOneMemberRSStatisticCert_inhabited is the one-statement nonempty theorem that cites this def as its witness, giving a single exportable fact for the verification layer.
In the Recognition framework the comparison is against the phi-ladder amplitude scale $\varphi^{-44}$ (log form), not a free fit parameter. The module is careful that this is amplitude-scale comparison only: it does not identify $\log A_{t_0}$ as the final RS echo observable and does not produce an archive-wide likelihood. It closes a structural verification node (dated 2026-05-22) with zero sorry and zero new RS-internal axioms, feeding any later multi-member or likelihood-layer certificates that need a typed one-event seed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.