phiMean
plain-language theorem explainer
Records the sample mean of the ringdown phase field φ_t_0 from one GWTC-3 HDF5 posterior as the real constant 3.1523706. Downstream sign and certificate lemmas cite it to lock the extracted summary against the schema. The body is a bare numeric definition from the companion Python range-read, not a derived identity.
Claim. The arithmetic mean of the posterior samples of the ringdown phase parameter $\phi_{t_0}$ extracted from the GWTC-3 member is the real number $3.1523706$.
background
The module freezes the first posterior-summary statistics from a single GWTC-3 ringdown HDF5 file (member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, 15114 samples, 7 fields). Fields include $\psi$, $\log A_{t_0}$, $f_{t_0}$, $\tau_{t_0}$, $\phi_{t_0}$, $\log L$, and $\log\mathrm{Prior}$.
This constant is the reported mean of $\phi_{t_0}$. Companion extraction lives in papers/reproducibility/gwtc3_ringdown_hdf5_sample_summary.py. The module is structural only: it pins column names and basic numerical ranges for a later likelihood parser. It is not an RS echo or QNM likelihood claim. Status is zero sorry and zero new RS-specific axioms.
proof idea
Definitional constant: the real value is written literally as 3.1523706. No tactic proof, no lemma application. Downstream mean_signs unfolds the name and discharges positivity by norm_num.
why it matters
Feeds the local certificate structure GWTC3RingdownHDF5SampleSummaryCert, which equates summary metadata to the schema (member name, posterior path, sample and field counts) and asserts positive sample count. Also appears in mean_signs, which packages sign constraints on all seven field means (here $0 < \phi$ mean).
In the Recognition verification layer this is scaffolding for GWTC-3 ringdown ingestion, not a forcing-chain step (T0–T8) or mass-ladder claim. It only establishes that the extracted $\phi_{t_0}$ mean is positive and schema-aligned so later parsers can trust column identity and rough scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.