gwtc3RingdownHDF5SampleSummaryCert
plain-language theorem explainer
A packed certificate that the GWTC-3 ringdown HDF5 posterior summary (member rin/rin_S190727h..., 15114 samples, 7 fields) matches the schema and passes basic numerical sanity: positive counts, correct mean signs, and ordered f and tau quantiles. Verification authors cite it as the single inhabited witness for the summary layer. The definition only assembles already-proved equality, positivity, sign, and ordering lemmas plus the upstream schema certificate.
Claim. A certificate asserting that the GWTC-3 ringdown HDF5 sample summary agrees with the schema on member name, posterior path, sample count ($15114$), and field count ($7$); that both counts are positive; that the means satisfy $\psi>0$, $\log A<0$, $f>0$, $\tau>0$, $\phi>0$, $\log L>0$, and $\log\mathrm{Prior}=0$; that the frequency quantiles obey $f_{16}<f_{\mathrm{med}}<f_{84}$ (and likewise for $\tau$); and that the underlying schema certificate is inhabited.
background
This Verification module freezes the first posterior-summary statistics from a range-read GWTC-3 ringdown HDF5 file: member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, sample count $15114$, field count $7$, fields $\psi$, $\log A_{t_0}$, $f_{t_0}$, $\tau_{t_0}$, $\phi_{t_0}$, $\log L$, $\log\mathrm{Prior}$. Status is structural theorem (0 sorry, 0 RS-internal axiom).
The structure being inhabited packages schema equalities (member, path, counts), positivity of counts, sign constraints on the seven means, ordering of $f$ and $\tau$ quantiles, and availability of the upstream schema certificate. Module intent is explicit: one-member posterior summary only, not an RS echo/QNM likelihood; the goal is locked column names and basic ranges for a later likelihood parser.
Upstream, the schema module supplies a nonempty schema certificate. Local lemmas such as mean-sign constraints and $f$-quantile order are proved by unfolding the frozen constants and norm_num/decide.
proof idea
Pure structure-instance assembly. Each field of the summary certificate is filled by a named local lemma: member/path/count equalities (reflexivity-style), positivity of sample and field counts (decide after unfold), mean-sign conjunction (unfold then norm_num on the seven floats), $f$ and $\tau$ quantile orderings (same norm_num pattern), and the inhabited upstream schema certificate. No new arithmetic or case analysis occurs in this definition; it only wires closed facts into one record.
why it matters
The sole direct consumer is the one-statement nonempty theorem for the posterior-summary certificate, which is the export surface verification pipelines use as a single Lean witness that the range-read HDF5 summary is schema-consistent and numerically sane.
In the Recognition verification stack this closes the structural ingestion layer for one GWTC-3 ringdown member (closure dated 2026-05-22). It does not touch the forcing chain T0–T8, the J-cost or RCL, phi-ladder masses, or the alpha band; it is infrastructure so later QNM/echo likelihood parsers can trust column names and ranges. Numeric constants are frozen from the companion reproducibility script under papers/reproducibility/.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.