summaryMemberName
plain-language theorem explainer
Fixes the HDF5 archive member path for the first GWTC-3 ringdown posterior sample used in the verification layer: the S190727h one-mode PyRing run. Downstream certificates and equality lemmas cite this constant so schema strings stay synchronized with the extracted summary. The body is a literal string definition, not a derived claim.
Claim. The ringdown summary member name is the fixed string $\texttt{rin/rin\_S190727h\_pyring\_DS\_1mode\_10M.h5}$, naming the HDF5 member that holds the first extracted GWTC-3 ringdown posterior sample.
background
The module records structural facts about one GWTC-3 ringdown HDF5 posterior extract, not an RS echo or QNM likelihood. Status is a closed structural theorem layer: zero sorry, zero new RS-specific axioms. The extract targets member rin/rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, with 15114 samples and seven fields (psi, logA_t_0, f_t_0, tau_t_0, phi_t_0, logL, logPrior).
Companion reproducibility lives in papers/reproducibility/gwtc3_ringdown_hdf5_sample_summary.py. The point of these constants is to pin column names and basic numerical ranges so a later likelihood parser can trust the schema. The sibling schema module supplies the reference strings and counts that this summary is checked against.
proof idea
Definitional constant: the right-hand side is the literal member path string. No tactics, no lemmas. Downstream equality with the schema name is discharged by rfl once both sides are the same string literal.
why it matters
Anchors the member-name field of GWTC3RingdownHDF5SampleSummaryCert, which requires summaryMemberName = sampleMemberName together with matching posterior path, sample count, field count, and positivity of the sample count. The theorem summary_member_matches_schema is the one-line rfl witness for that equality.
In the broader verification stack this is plumbing for GWTC-3 ringdown data intake: establish that Lean’s recorded member path is exactly the schema’s member path before any physics-facing likelihood is attached. It does not itself encode Recognition-Science forcing (T0–T8), the J-cost, or mass-ladder claims; it only freezes the observational file identity those later layers will read.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.