summary_field_count_pos
plain-language theorem explainer
The GWTC-3 ringdown posterior summary records a strictly positive number of fields. Anyone assembling the sample-summary certificate cites this positivity side-condition. The proof unfolds the constant field count to 7 and discharges 0 < 7 by decision procedure.
Claim. The number of fields in the GWTC-3 ringdown HDF5 posterior summary is positive: $0 < 7$.
background
This module freezes the first posterior-summary statistics taken from one GWTC-3 ringdown HDF5 member (rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples). It is structural bookkeeping only: column names and basic counts for a later likelihood parser, not an RS echo or QNM fit.
The field count is the constant natural number 7, corresponding to the seven named posterior columns psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, and logPrior. Sample count is separately recorded as 15114. The companion Python script under papers/reproducibility/ is the extraction source of truth.
proof idea
One-line term-style proof: unfold the definition of the summary field count (the literal natural 7), then decide closes the inequality $0 < 7$.
why it matters
Positivity of the field count is a trivial but required side-condition in the packaged certificate gwtc3RingdownHDF5SampleSummaryCert, which bundles member, path, sample-count, and field-count schema matches. Downstream consumers of that certificate can assume the summary is non-vacuous in its column dimension without re-proving arithmetic. The module itself is marked structural closure (zero sorry, zero new RS axioms); this lemma is one of the elementary Nat facts that keep the certificate well-formed. It does not touch the forcing chain, RCL, or mass ladder; it only anchors the verification layer that will later feed ringdown data into RS tests.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.