fQ16
plain-language theorem explainer
Records the empirical 16% quantile of the ringdown frequency posterior from the GWTC-3 HDF5 member rin_S190727h (one-mode pyring run) as the real constant 172.53798. Verification and data-binding proofs cite it when checking quantile order and packaging the sample-summary certificate. The body is a bare numeric definition extracted by the companion Python range-read script.
Claim. The 16th-percentile value of the ringdown frequency posterior samples $f_{t_0}$ extracted from the GWTC-3 HDF5 member is the real constant $172.53798$.
background
The 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, 15114 samples, seven fields (psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, logPrior). Companion extraction lives in papers/reproducibility/gwtc3_ringdown_hdf5_sample_summary.py.
This constant is the lower empirical quantile of the frequency column $f_{t_0}$. Sibling means (fMean, tauMean, logAMean, ...) and the matching median and 84% quantile sit beside it so that later theorems can assert elementary order and positivity facts without re-opening the HDF5 file. The module is structural only: column names and numerical ranges for a future likelihood parser, not an RS echo or QNM model.
proof idea
Definitional constant: the right-hand side is the literal real 172.53798 written into Lean after offline extraction. No tactic proof, no lemmas. Downstream f_quantile_order unfolds this name together with the median and 84% quantile and discharges the two strict inequalities by norm_num.
why it matters
Pins the lower frequency quantile used by f_quantile_order (proving $f_{Q16} < f_{\mathrm{median}} < f_{Q84}$) and by the packaged certificate GWTC3RingdownHDF5SampleSummaryCert and the one-statement summary theorem. Those parents establish that the range-read sample is non-degenerate and schema-aligned before any Recognition-Science likelihood is attached. The module status is structural closure (0 sorry, 0 new RS axioms); this constant is pure data binding, not a forcing-chain or RCL step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.