f_quantile_order
plain-language theorem explainer
The 16th, 50th, and 84th percentiles of the ringdown frequency posterior from the certified GWTC-3 HDF5 sample obey the natural order f16 < fmed < f84. Anyone citing the one-member posterior summary for rin_S190727h uses this as a basic sanity check on the extracted quantiles. The proof unfolds three numeric constants and discharges both inequalities by norm_num.
Claim. The frequency quantiles from the GWTC-3 ringdown posterior sample satisfy $f_{16} < f_{\mathrm{med}} < f_{84}$, where $f_{16} = 172.53798$, $f_{\mathrm{med}} = 345.41413$, and $f_{84} = 819.88387$.
background
This module freezes the first posterior-summary statistics read from a single GWTC-3 ringdown HDF5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples). It records sample count 15114, seven fields (psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, logPrior), and selected means and quantiles. The purpose is structural: lock column names and numerical ranges for a later likelihood parser, not to assert an RS echo or QNM fit.
The three constants used here are the 16th percentile, median, and 84th percentile of the frequency field f_t_0, written as real literals 172.53798, 345.41413, and 819.88387. In gravitational-wave ringdown analyses those three numbers are the usual asymmetric-error anchors around the median frequency.
proof idea
One-line numeric discharge. Unfold the three definitions to their real literals, then apply norm_num to both strict inequalities. No lemmas beyond the unfolded constants are required.
why it matters
The inequality is a certified sanity constraint on the frequency column of the one-member HDF5 summary. It is consumed by the aggregate certificate gwtc3RingdownHDF5SampleSummaryCert and by the bundled one-statement theorem gwtc3_ringdown_hdf5_sample_summary_one_statement, which packages sample counts, field counts, and sign/order facts into a single conjunction. Within the Verification domain this is scaffolding for later RS-facing ringdown likelihood work: it proves the extracted quantiles are ordered as a real posterior summary must be, with zero sorry and no new RS axioms. It does not itself touch the forcing chain (T0–T8), RCL, or the mass ladder; it only freezes observational input that those layers may later consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.