GWTC3RingdownOneMemberRSStatisticCert
plain-language theorem explainer
Certificate packing six claims for one GWTC-3 ringdown member: the RS target log(phi^{-44}) sits above the posterior 95% quantile of log A, outside the central 90% and 68% intervals, more than two std above the mean, with sample fraction above target under 0.001, plus a nonempty HDF5 summary cert. Verification authors cite it for the one-member amplitude-scale comparison. Structure of Prop fields only; inhabitants discharge each inequality from frozen numeric defs.
Claim. A certificate is six assertions on the one-member GWTC-3 ringdown posterior for $\log A_{t_0}$: the RS target $\log(\varphi^{-44})$ exceeds the $95\%$ quantile; it lies outside the central $90\%$ interval $[q_{0.05},q_{0.95}]$ and outside the central $68\%$ interval $[q_{0.16},q_{0.84}]$; the $z$-score versus the posterior mean exceeds $2$; the sample fraction above the target is less than $0.001$; and a nonempty HDF5 sample-summary certificate exists for the member schema.
background
This module records the first explicitly RS-referenced statistic on a range-read GWTC-3 ringdown posterior: member 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 summaries: mean $\approx-22.245$, std $\approx0.398$, median $\approx-22.212$, with quantiles frozen as reals ($q_{0.05}\approx-22.911$, $q_{0.16}\approx-22.720$, $q_{0.84}\approx-21.825$, $q_{0.95}\approx-21.638$).
Sibling defs fix residuals, $z$ from the mean, and the sample fraction above target ($0.000331$). Upstream, the HDF5 sample-summary certificate checks member name, posterior path, sample count, and field count against the schema, with positive sample count. Setting is one-member amplitude-scale comparison only; it does not identify $\log A_{t_0}$ as the final RS echo observable or compute an archive-wide likelihood.
proof idea
No proof body: this is a structure whose fields are propositions. An inhabitant supplies proofs of each field inequality against the frozen numeric defs (quantile constants, $z$ from mean, fraction above target, RS log-phi target) plus a witness that the HDF5 sample-summary certificate is nonempty. Downstream, the concrete certificate value fills those fields from named inequality lemmas (target above q95, outside 90% and 68% intervals, $z>2$, fraction bound).
why it matters
Packages the one-member RS amplitude-scale comparison into one certificate type used by the concrete certificate value, the inhabitedness theorem, and the one-statement conjunction that collapses the headlines: target above $q_{0.95}$, $z>2$, fraction $<0.001$, and nonempty certificate. In the Recognition verification layer this is the first closed (0 sorry, 0 new RS axioms) link from a concrete GWTC-3 ringdown posterior column to the phi-ladder amplitude target $\log(\varphi^{-44})$. It does not touch the forcing chain T0-T8 or RCL; it is empirical packaging of a phi-power scale against LIGO/Virgo ringdown posteriors. Open questions left explicit: whether $\log A_{t_0}$ is the correct final RS echo amplitude observable, and archive-wide likelihoods beyond this single member.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.