psiMean
plain-language theorem explainer
The sample mean of the ringdown polarization angle ψ from the GWTC-3 S190727h HDF5 posterior is fixed at 1.5465191. GW verification and ringdown-summary pipelines cite this constant when checking sign and range constraints on extracted fields. It is a bare real literal with no proof obligations.
Claim. The sample mean of the ringdown polarization angle $\psi$ from the one-member GWTC-3 ringdown HDF5 posterior extract equals $1.5465191$.
background
This module freezes the first posterior-summary statistics read from a GWTC-3 ringdown HDF5 file: member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, 15114 samples, seven fields (ψ, logA_t_0, f_t_0, τ_t_0, φ_t_0, logL, logPrior). Companion extraction lives in papers/reproducibility/gwtc3_ringdown_hdf5_sample_summary.py.
The local goal is structural only: lock column names and basic numerical ranges for a later likelihood parser. It is not an RS echo or QNM likelihood claim. Zero sorry and no new RS-specific axioms.
psiMean is the recorded mean of the ψ column from that single-member extract.
proof idea
Bare definition: the real constant is set equal to the decimal 1.5465191 produced by the external reproducibility script. No lemmas, tactics, or algebraic reduction.
why it matters
Feeds mean_signs, which proves the seven field-mean sign constraints
$0 < \psi$, $\log A < 0$, $0 < f$, $0 < \tau$, $0 < \phi$, $0 < \log L$, $\log\mathrm{Prior} = 0$
by unfolding the mean constants and norm_num. Also sits in the certificate structure that ties summary metadata (member name, path, sample count, field count) to the schema. Supplies the numerical anchor needed before any later RS-side ringdown comparison; the module itself remains one-member posterior summary only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.