posterior_summary_available
plain-language theorem explainer
Existence of a schema-matching certificate for the range-read GWTC-3 ringdown HDF5 posterior sample (member rin_S190727h, dataset /EXP6/posterior_samples). Anyone citing the one-member RS amplitude statistic needs this as the data-availability gate. Proof is a one-line term wrapper of the upstream inhabited certificate.
Claim. There exists a certificate that the range-read GWTC-3 ringdown HDF5 posterior summary matches its schema: member name, posterior path, sample count, and field count agree with the fixed sample identifiers, and the sample count is strictly positive.
background
This module records the first explicitly RS-referenced statistic on a single GWTC-3 ringdown posterior table: 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 posterior mean, std, median, quantiles, residual, $z$-score, and fraction above target are fixed numeric constants in the module.
Upstream, GWTC3RingdownHDF5SampleSummaryCert is a structure whose fields assert schema agreement: member name, posterior path, sample count, and field count match the fixed sample identifiers, and the sample count is positive. The companion theorem gwtc3RingdownHDF5SampleSummaryCert_inhabited supplies a concrete inhabitant (doc: "One-statement posterior-summary theorem for the range-read HDF5 sample").
The present declaration is the local availability gate: before any RS amplitude comparison is stated, the posterior summary certificate must be nonempty.
proof idea
One-line term proof. It applies the upstream theorem that inhabits GWTC3RingdownHDF5SampleSummaryCert (the concrete certificate built from the fixed sample summary constants) and thereby witnesses Nonempty of that structure type. No further tactics or algebraic steps.
why it matters
Feeds the master certificate gwtc3RingdownOneMemberRSStatisticCert, which packages the RS amplitude comparisons: target above the 95% quantile, outside the central 90% and 68% intervals, and $z > 2$ from the posterior mean. Without nonempty posterior-summary availability, that master cert cannot be assembled.
In the Recognition framework this is verification scaffolding, not a forcing-chain step (T0–T8). It anchors the first one-member amplitude-scale comparison of ringdown $\log A$ against the $\varphi$-ladder target $\log(\varphi^{-44})$. The module status is structural theorem: zero sorry, zero new RS-internal axioms. It does not claim that $\log A_{t_0}$ is the final RS echo observable, nor an archive-wide likelihood.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.