summary_sample_count_pos
plain-language theorem explainer
The GWTC-3 ringdown posterior sample count recorded in this module is strictly positive. Verification and certificate authors cite it when assembling the one-member HDF5 summary certificate. The proof unfolds the Nat constant 15114 and closes by decidable comparison.
Claim. The recorded GWTC-3 ringdown posterior sample count satisfies $0 < 15114$.
background
This module freezes the first posterior-summary statistics taken from a range-read GWTC-3 ringdown HDF5 file (member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples). It is structural bookkeeping only: column names and basic numerical ranges for a later likelihood parser, not an RS echo or QNM likelihood.
The sample count is the Nat constant summarySampleCount := 15114, extracted alongside seven fields (psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, logPrior). Companion extraction lives in the reproducibility script named in the module doc. Status is full structural closure: zero sorry, zero new RS-specific axioms.
proof idea
One-line tactic proof. Unfold the definition of the sample-count constant to the literal natural 15114, then decide discharges $0 < 15114$ by the decidable order on Nat. No lemmas beyond definitional unfolding are required.
why it matters
Feeds the certificate bundle gwtc3RingdownHDF5SampleSummaryCert, which packages member, path, sample-count, and field-count schema matches for the one-member posterior summary. Without a proved positive sample count, the schema match for sample cardinality cannot be assembled as a closed certificate object.
In the broader Verification domain this is infrastructure for GWTC-3 ringdown data hygiene, not a forcing-chain or mass-ladder claim. It does not touch T0–T8, RCL, or the alpha band; it only locks the empirical sample size that later parsers will read against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.