logAMean
plain-language theorem explainer
Records the sample mean of the log-amplitude field logA_t_0 from one GWTC-3 ringdown HDF5 posterior as the real constant -22.244585. Verification and GW data workers cite it when wiring column ranges into the likelihood parser. The body is a bare numeric definition, not a derived identity.
Claim. The posterior-sample mean of the ringdown log-amplitude field $\log A_{t_0}$ extracted from the GWTC-3 member is the real number $-22.244585$.
background
The module freezes first-pass summary statistics from a range-read GWTC-3 ringdown HDF5 file (member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, 15114 samples, seven fields). Companion Python lives under papers/reproducibility/. This is structural bookkeeping only: column names and numerical ranges for a later likelihood parser, not an RS echo or QNM fit.
Among the seven fields is logA_t_0, the log of the ringdown amplitude at a reference time. Sibling constants pin the other field means (psi, frequency, damping time, phase, log-likelihood, log-prior) and the schema identifiers (member name, path, sample and field counts). No RS-native units or forcing-chain landmarks enter here.
proof idea
Definitional constant: the real literal -22.244585 is assigned directly. No lemmas, tactics, or algebraic reduction. Downstream theorems such as mean_signs simply unfold this name and discharge the inequality logAMean < 0 by norm_num.
why it matters
Supplies the concrete log-amplitude mean that mean_signs and gwtc3_ringdown_hdf5_sample_summary_one_statement quote when they assert logAMean < 0 together with positivity of frequency and damping-time means. The certificate structure GWTC3RingdownHDF5SampleSummaryCert ties the same summary block to the schema (member, path, counts). That one-statement theorem is the module's closure artifact: zero sorry, zero new RS axioms, establishing that the range-read sample is non-vacuous and sign-consistent before any RS likelihood is attached. It does not touch T0–T8, RCL, or the phi ladder; it only locks empirical column ranges the parser will later consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.