fQ84
plain-language theorem explainer
Records the empirical 84th percentile of the ringdown frequency posterior from the GWTC-3 HDF5 member rin_S190727h (one-mode pyring run): $f_{84}=819.88387\,\mathrm{Hz}$. Downstream quantile-order and sample-summary certificates cite this constant. It is a literal real binding extracted by the companion Python summary script, not a derived RS prediction.
Claim. The 84th percentile of the posterior samples for the ringdown frequency $f_{t_0}$ in the range-read GWTC-3 HDF5 dataset is the real constant $819.88387$.
background
This module freezes the first posterior-summary statistics from a single GWTC-3 ringdown HDF5 member: rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, with 15114 samples and seven fields (psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, logPrior). The companion script papers/reproducibility/gwtc3_ringdown_hdf5_sample_summary.py computes means and selected quantiles offline; Lean only stores the resulting numbers.
The frequency field $f_{t_0}$ is the damped-sinusoid ringdown frequency in the one-mode fit. Alongside the mean and the 16th percentile, the 84th percentile is kept so that the empirical central interval can be checked by a pure numerical inequality. The module is structural verification only: column names and basic ranges for a later likelihood parser, not an RS echo or QNM likelihood.
proof idea
Definitional binding: the real literal 819.88387 is assigned to the constant. No tactic proof and no lemmas. Downstream, f_quantile_order unfolds this constant with fQ16 and fMedian and discharges $f_{16}<f_{\mathrm{med}}<f_{84}$ by norm_num.
why it matters
Pins the upper edge of the empirical frequency quantile triple used by f_quantile_order (proving $f_{16}<f_{\mathrm{med}}<f_{84}$) and by the bundled certificate GWTC3RingdownHDF5SampleSummaryCert and the one-statement summary theorem gwtc3_ringdown_hdf5_sample_summary_one_statement. Those objects establish that the range-read HDF5 sample has the expected schema, positive sample count, and sane numerical ranges before any RS ringdown likelihood is attached.
In the broader Recognition verification stack this is infrastructure, not a forcing-chain step: it does not invoke J-cost, $\varphi$, the eight-tick octave, or the mass ladder. It closes a reproducibility hinge so later QNM or echo analyses can cite a machine-checked sample summary rather than an untracked notebook number.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.