gwtc3_ringdown_hdf5_sample_summary_one_statement
plain-language theorem explainer
Packages the GWTC-3 ringdown HDF5 posterior summary into one conjunction: 15114 samples, 7 fields, positive frequency and damping-time means, negative log-amplitude mean, zero log-prior mean, ordered f and tau quantiles, and a nonempty certificate. Verification authors cite it as the closed one-statement audit of the range-read sample. Term-mode proof joins rfl equalities, mean-sign projections, quantile-order lemmas, and the certificate inhabitant.
Claim. The recorded GWTC-3 ringdown HDF5 posterior has sample count $15114$ and field count $7$; the mean ringdown frequency and mean damping time are positive; the mean log-amplitude is negative; the mean log-prior equals $0$; the $16\%$, median, and $84\%$ quantiles of frequency are strictly ordered, and likewise for damping time; and the posterior-summary certificate structure is inhabited.
background
This module records the first posterior-summary statistics from a range-read GWTC-3 ringdown HDF5 file: member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, with fields psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, and logPrior. Status is structural theorem (zero sorry, zero new RS axioms). The aim is to fix column names and basic numerical ranges for a later likelihood parser, not to state an RS echo or QNM likelihood.
Concrete constants include frequency mean $\approx 420.95$, median $\approx 345.41$, and $16%/84%$ quantiles $\approx 172.54$ and $\approx 819.88$, with parallel tau statistics. The certificate structure bundles schema equalities (member name, posterior path, sample and field counts) with positivity of those counts and the full seven-field mean sign pattern.
proof idea
Term proof that builds the nine-way conjunction directly. Sample-count and field-count equalities are rfl against the literal definitions. The four mean-sign claims (positive $f$ and $\tau$ means, negative log-amplitude mean, zero log-prior mean) are projections out of a pre-proved mean_signs bundle. Frequency and damping-time quantile orderings are the lemmas f_quantile_order and tau_quantile_order (each unfolds the decimal constants and finishes by norm_num). Nonemptiness of the certificate is the inhabitant gwtc3RingdownHDF5SampleSummaryCert_inhabited.
why it matters
Closes the one-member GWTC-3 ringdown posterior audit as a single proved statement, matching the module claim of structural closure with zero sorry and zero new RS-specific axioms. It lives in the Verification domain as infrastructure: a machine-checkable anchor for the companion Python reproducibility script and for any later parser that will compare ringdown posteriors to Recognition Science QNM or echo predictions. No downstream consumers are wired yet (used_by empty). The result is not itself a physics claim about the forcing chain, phi-ladder masses, or the alpha band; it only locks the HDF5 schema and numerical ranges needed before those comparisons can be stated formally.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.