sample_summary_available
plain-language theorem explainer
The GWTC-3 ringdown HDF5 posterior sample summary is certified as present: the schema-matching certificate type is inhabited. Downstream one-member damping statistic certificates cite this to ground the range-read sample before comparing QNM damping to the RS target 1/φ. The proof is a one-line term that reuses the upstream inhabited instance.
Claim. The type of certificates asserting that the GWTC-3 ringdown HDF5 sample summary matches its schema is nonempty: member name, posterior path, sample count, and field count agree with the fixed schema values, and the sample count is strictly positive.
background
This module records a one-member GWTC-3 ringdown statistic. Posterior samples of fundamental QNM frequency $f_{t_0}$ and damping time $\tau_{t_0}$ are mapped to the per-cycle damping ratio $\mathrm{damping_per_cycle}=\exp(-1/(f_{t_0}\tau_{t_0}))$. The Recognition Science structural echo-damping target is $1/\varphi\approx 0.618$.
Upstream, GWTC3RingdownHDF5SampleSummaryCert packages five schema facts for the range-read member rin/rin_S190727h_pyring_DS_1mode_10M.h5: member name, posterior path, sample count, field count, and positivity of the sample count. The companion theorem states that this certificate type is inhabited by an explicit witness.
The present declaration simply re-exports that nonemptiness into the damping-statistic module so later fields (means, quantiles, $z$-score versus the RS target) can assume the sample summary exists.
proof idea
One-line term proof. It applies the upstream theorem that constructs an explicit inhabitant of the sample-summary certificate structure, thereby discharging Nonempty for that type. No further tactics or algebraic work.
why it matters
The master one-member damping certificate structure requires the RS target $1/\varphi$ to lie inside the central 68% and 90% damping intervals, a mean-based $z$-score below one, and a valid fraction-below-target. Building that certificate (and its packaged def) depends on knowing the HDF5 sample summary is available; this theorem supplies that precondition.
In the broader verification layer it is structural bookkeeping, not a new physics claim: it closes the data-presence gate for the first physically mapped one-member GWTC-3 ringdown damping comparison against the RS echo-damping landmark $\varphi^{-1}$. It does not touch the forcing chain T0–T8, RCL, or mass ladder; it only anchors the observational side of the damping check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.