GWTC3RingdownHDF5SampleSummaryCert
plain-language theorem explainer
A certificate structure bundling the numerical posterior summary of one GWTC-3 ringdown HDF5 member (S190727h, 15114 samples, 7 fields) against its schema. Downstream damping and RS-statistic modules cite it to guarantee that means, medians, and quantiles are well-formed before comparing to Recognition targets. As a structure, it is pure interface: no proof body, only field obligations.
Claim. A sample-summary certificate is a record asserting: the summary member name and posterior path equal the schema constants; sample count equals $15114$ and field count equals $7$, both positive; the field means satisfy $\psi>0$, $\log A<0$, $f>0$, $\tau>0$, $\phi>0$, $\log L>0$, $\log\mathrm{Prior}=0$; the frequency and damping quantiles are strictly ordered $q_{16}<\mathrm{median}<q_{84}$; and a nonempty schema certificate exists.
background
The module freezes the first range-read posterior summary from the GWTC-3 ringdown release. The member is rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, with 15114 draws over seven columns: $\psi$, $\log A_{t_0}$, $f_{t_0}$, $\tau_{t_0}$, $\phi_{t_0}$, $\log L$, $\log\mathrm{Prior}$. Companion Python extracts the floats; Lean only records them.
Upstream, GWTC3RingdownHDF5SampleSchemaCert already pins the member string, compressed/uncompressed sizes, and the constants posteriorSamplesCount = 15114, posteriorFieldCount = 7, and the dataset path. Summary-side defs such as fMean := 420.95381 (and siblings for medians and quantiles) are the numeric payload this certificate constrains.
Local status is structural: zero sorry, zero new RS axioms. The point is column identity and basic range hygiene for a later likelihood parser, not an RS echo or QNM fit.
proof idea
No proof body: the declaration is a structure. Each field is a Prop obligation (equalities to schema constants, positivity of counts, sign pattern on the seven means, strict quantile sandwiches for $f$ and $\tau$, and Nonempty of the schema cert). Inhabitation is supplied later by the concrete value gwtc3RingdownHDF5SampleSummaryCert, which fills every field from the sibling equality lemmas and numeric facts.
why it matters
This is the hinge between raw HDF5 schema facts and the one-member physics comparisons. gwtc3RingdownHDF5SampleSummaryCert_inhabited and the one-statement theorem package the counts and sign facts for citation. Downstream, sample_summary_available in the damping-statistic module simply re-exports that nonemptiness, and GWTC3RingdownOneMemberDampingStatisticCert then checks whether an RS damping target sits inside the empirical 68% and 90% bands. The parallel RS-statistic cert uses the same availability fact before testing a $\log A$ target (tied to $\phi^{-44}$ scale ideas) against posterior quantiles.
In the broader Verification domain this is data hygiene, not a forcing-chain step (T5–T8). It does not invoke J-cost, RCL, or the eight-tick octave; it only makes the GWTC-3 ringdown posterior safe to quote when those RS targets are later scored.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.