tauMedian
plain-language theorem explainer
Median ringdown damping time τ from the GWTC-3 HDF5 posterior for S190727h is the literal real 0.021072448. Downstream quantile-order and one-statement summary certificates cite it as the middle τ statistic. The declaration is a bare constant definition, not a derived identity.
Claim. The sample median of the ringdown damping time $\tau_{t_0}$ from the range-read GWTC-3 posterior (`rin/rin_S190727h_pyring_DS_1mode_10M.h5`, dataset `/EXP6/posterior_samples`) equals $0.021072448$.
background
This module freezes the first posterior-summary numbers pulled from one GWTC-3 ringdown HDF5 member: 15114 samples, seven fields (psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, logPrior). Companion Python under papers/reproducibility/ performs the range-read; Lean only records the extracted floats.
Here $\tau_{t_0}$ is the damped-sinusoid decay time of the single-mode ringdown fit, in the units of the released posterior. The median sits between the 16% and 84% quantiles (tauQ16, tauQ84) that the same file also hard-codes. The module is structural bookkeeping for column names and numerical ranges needed by a later likelihood parser, not an RS echo or QNM prediction.
proof idea
Definitional constant: the real literal 0.021072448 is assigned with no proof obligations. Downstream tau_quantile_order unfolds this name beside tauQ16 and tauQ84 and closes the two strict inequalities by norm_num.
why it matters
Supplies the middle τ anchor for tau_quantile_order (tauQ16 < tauMedian < tauQ84) and is referenced by the master certificate structure GWTC3RingdownHDF5SampleSummaryCert and the bundled theorem gwtc3_ringdown_hdf5_sample_summary_one_statement. Those objects pin sample count, field count, and basic sign/positivity facts so a later GWTC-3 ringdown likelihood parser can trust column identity and scale. 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.