logPriorMean
plain-language theorem explainer
Records the sample mean of the log-prior column from the GWTC-3 ringdown HDF5 posterior as exactly 0. Downstream sign checks and the one-statement summary certificate cite this constant. It is a one-line numeric definition, not a derived identity.
Claim. The sample mean of the $\log\mathrm{Prior}$ field in the range-read GWTC-3 ringdown posterior equals $0$.
background
This module freezes the first posterior-summary statistics from one GWTC-3 ringdown HDF5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples). The extract has 15114 samples and seven fields: $\psi$, $\log A_{t_0}$, $f_{t_0}$, $\tau_{t_0}$, $\phi_{t_0}$, $\log L$, and $\log\mathrm{Prior}$.
The purpose is structural only: lock column names and basic numerical ranges for a later likelihood parser. It is not an RS echo or QNM likelihood. Companion extraction lives in papers/reproducibility/gwtc3_ringdown_hdf5_sample_summary.py.
Sibling constants hold the other field means (psiMean, logAMean, fMean, tauMean, phiMean, logLMean). This entry is the $\log\mathrm{Prior}$ mean.
proof idea
Literal definition: the real constant is set to $0$. No lemmas, tactics, or algebraic reduction. Downstream mean_signs unfolds the name and discharges the equality by norm_num.
why it matters
Feeds three local consumers: the structure GWTC3RingdownHDF5SampleSummaryCert (schema and count match obligations), the theorem mean_signs (which asserts among other inequalities that this mean equals 0), and gwtc3_ringdown_hdf5_sample_summary_one_statement (the bundled one-statement posterior-summary claim).
In the Recognition verification layer this is plumbing, not physics: it pins the empirical $\log\mathrm{Prior}$ column mean so later parsers and certificates can refer to a named constant rather than a magic number. It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it only stabilizes GWTC-3 ringdown sample bookkeeping ahead of any RS likelihood comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.