fMean
plain-language theorem explainer
Records the sample mean of the ringdown frequency field f_t_0 as the real constant 420.95381 Hz-scale units from the GWTC-3 HDF5 posterior. Verification and GWTC-3 ringdown pipeline authors cite it when locking numerical ranges into Lean certificates. It is a bare numeric definition with no proof obligations.
Claim. The mean of the posterior samples for the ringdown frequency $f_{t_0}$ extracted from the GWTC-3 member is the real number $420.95381$.
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). Sample count is 15114 across seven fields: $\psi$, $\log A_{t_0}$, $f_{t_0}$, $\tau_{t_0}$, $\phi_{t_0}$, $\log L$, and $\log\mathrm{Prior}$.
This constant is the empirical mean of the frequency column $f_{t_0}$. Companion values (means of amplitude, damping time, phases, likelihood) sit beside it. The module is structural only: it pins column names and numerical ranges for a later likelihood parser, not an RS echo or QNM fit. Status is zero sorry and zero new RS axioms.
proof idea
Pure definition: the real literal $420.95381$ is assigned with no tactics, lemmas, or computation inside Lean. Downstream proofs that need positivity simply unfold this name and discharge with norm_num.
why it matters
Feeds three local consumers: the sign bundle mean_signs (which asserts $0 < fMean$ among other inequalities), the certificate structure GWTC3RingdownHDF5SampleSummaryCert that ties summary metadata to the schema, and the one-statement theorem gwtc3_ringdown_hdf5_sample_summary_one_statement that packages sample count, field count, and mean-sign facts. In the Recognition verification layer this is scaffolding for GWTC-3 ringdown ingestion, not a forcing-chain (T0–T8) or RCL step. It closes the numeric half of the structural theorem dated 2026-05-22 so later QNM/echo likelihood code can trust the column ranges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.