tauMean
plain-language theorem explainer
Records the sample mean of the ringdown damping time τ_t0 from the range-read GWTC-3 HDF5 posterior (rin_S190727h, 15114 samples) as the real constant 0.022773848. Downstream sign and certificate lemmas cite it to pin positivity of τ. The body is a bare numeric definition, not a derived claim.
Claim. The empirical mean of the ringdown damping-time coordinate $\tau_{t_0}$ over the GWTC-3 posterior sample is the real number $0.022773848$.
background
The module freezes first-pass summary statistics from one GWTC-3 ringdown HDF5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples). Seven posterior fields are named: $\psi$, $\log A_{t_0}$, $f_{t_0}$, $\tau_{t_0}$, $\phi_{t_0}$, $\log L$, and $\log\mathrm{Prior}$, with sample count 15114.
$\tau_{t_0}$ is the damping-time coordinate of the single-mode ringdown fit. This constant is the arithmetic mean of that column as extracted by the companion Python script; it is bookkeeping for column identity and numeric range, not an RS QNM or echo likelihood.
Sibling means (fMean, psiMean, logAMean, etc.) play the same role for the other columns. Schema names and counts live in the imported sample-schema module.
proof idea
Pure definition: the identifier is bound to the literal real 0.022773848. No tactic proof, no lemma application. Downstream mean_signs unfolds this binding and discharges 0 < tauMean by norm_num.
why it matters
Feeds the structural certificate GWTC3RingdownHDF5SampleSummaryCert and the one-statement summary theorem, which conjoin sample/field counts with sign constraints including 0 < tauMean. Also appears in mean_signs, which packages positivity (and related sign) facts for all seven field means.
In the Verification lane this pins that the extracted $\tau$ mean is positive and in a physically plausible ringdown range before any RS echo/QNM likelihood is attached. Module status is structural closure (0 sorry, 0 new RS axioms); it does not yet connect to the forcing chain (T0–T8), RCL, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.