tau_quantile_order
plain-language theorem explainer
The 16th, 50th, and 84th percentiles of the ringdown damping-time posterior satisfy the strict order q16 < median < q84. Anyone wiring GWTC-3 ringdown sample summaries into a certified schema cites this. The proof unfolds three numeric defs and discharges the inequalities by norm_num.
Claim. For the range-read GWTC-3 ringdown posterior on $\tau_{t_0}$, the sample quantiles obey $q_{16}(\tau) < \mathrm{median}(\tau) < q_{84}(\tau)$, with the concrete values $0.0076396112 < 0.021072448 < 0.039327675$.
background
This module freezes the first posterior-summary statistics taken from a single GWTC-3 ringdown HDF5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, 15114 samples, 7 fields). It is structural bookkeeping only: column names and basic numerical ranges for a later likelihood parser, not an RS echo or QNM fit.
Among the frozen fields is the damping time $\tau_{t_0}$. Three constants record its sample quantiles: tauQ16 $= 0.0076396112$, tauMedian $= 0.021072448$, and tauQ84 $= 0.039327675$. The present theorem asserts the elementary order relation among those three numbers, which any well-formed unimodal posterior summary must satisfy.
proof idea
Term-mode proof by direct evaluation. Unfold the three definitions to their decimal literals, then apply norm_num to discharge both strict inequalities on concrete reals. No lemmas beyond the definitions themselves are required.
why it matters
Feeds the master certificate gwtc3RingdownHDF5SampleSummaryCert and the bundled one-statement theorem gwtc3_ringdown_hdf5_sample_summary_one_statement, which package schema matches, sample/field counts, and sign/range facts for the range-read HDF5 summary. Ordering of the $\tau$ quantiles is a minimal sanity check that the frozen numbers are a coherent posterior summary rather than a scrambled table. The module is marked structural closure (0 sorry, 0 new RS axioms); it does not yet touch RS landmarks (T0–T8, RCL, phi-ladder masses), only the data interface those later comparisons will need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.