logLMean
plain-language theorem explainer
Records the sample mean of the log-likelihood column from one GWTC-3 ringdown posterior HDF5 member as the real constant 58695.535. Verification and GW data pipelines cite it when locking column ranges and sign checks before any RS echo or QNM likelihood is built. The body is a bare numeric definition, not a derived proof.
Claim. The arithmetic mean of the $\log L$ field over the $15114$ posterior samples in the GWTC-3 ringdown member is the real number $58695.535$.
background
The module freezes the first posterior-summary statistics read from a single GWTC-3 ringdown HDF5 file (member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples). Sample count is 15114 and field count is 7: $\psi$, $\log A_{t_0}$, $f_{t_0}$, $\tau_{t_0}$, $\phi_{t_0}$, $\log L$, and $\log\mathrm{Prior}$.
Companion extraction lives in the reproducibility script; the Lean side only stores the resulting scalars so later parsers have fixed names and numerical ranges. This is structural bookkeeping for one member, not an RS echo or quasinormal-mode likelihood.
Sibling constants hold the other field means and selected quantiles. Schema identifiers from the imported sample-schema module supply the expected member name, path, and counts that the summary must match.
proof idea
Pure definition: the identifier is bound to the literal real $58695.535$. No tactics, no lemmas, no computation inside Lean. Downstream theorems unfold the name and discharge numeric goals with norm_num.
why it matters
Feeds the certificate structure that asserts member name, posterior path, sample count, and field count agree with the schema, and that the sample count is positive. Also appears in the mean-sign theorem, which proves the log-likelihood mean is strictly positive (together with sign constraints on the other field means and $\log\mathrm{Prior}$ mean equal to zero).
In the Recognition verification layer this locks the empirical column ranges needed before any later RS-facing ringdown likelihood parser is written. It does not itself invoke the forcing chain, RCL, or mass ladder; it is infrastructure so those claims can be checked against real GWTC-3 posterior samples without silent schema drift.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.