gwtc3RingdownHDF5SampleSchemaCert
plain-language theorem explainer
Bundles the schema-level facts for one inspected GWTC-3 ringdown HDF5 posterior member (the smallest .h5 in the public ZIP) into a single certificate value. Verification and reproducibility authors cite it when they need a machine-checked record that the member name, byte sizes, object split, and posterior dataset path match the live range-read metadata. Construction is a structure instance that wires seven local rfl/decide lemmas plus the upstream ZIP-schema inhabitation.
Claim. There is a certificate recording that the inspected GWTC-3 ringdown HDF5 member is named $\mathtt{rin/rin\_S190727h\_pyring\_DS\_1mode\_10M.h5}$, that its compressed and uncompressed sizes are positive with uncompressed strictly larger, that group count plus dataset count equals the HDF5 object count, that the posterior dataset path is $\mathtt{/EXP6/posterior\_samples}$, that posterior sample and field counts are positive, and that the companion ringdown ZIP schema certificate is inhabited.
background
The module freezes a one-member schema inspection of the public GWTC-3 ringdown ZIP without pulling the full 1.44 GB archive. Method: HTTP range-read the ZIP central directory, pick the smallest .h5 member, range-read only its local header and compressed payload, inflate locally, and inspect with h5py. Live numbers include compressed size 679110, uncompressed 931208, 97 HDF5 objects (14 groups, 83 datasets), and key posterior path /EXP6/posterior_samples with 15114 samples and 7 fields.
The certificate structure packages those frozen constants as propositions: member name equality, positivity and ordering of byte sizes, additive split of object counts, named posterior path, and positivity of sample and field counts. A final field requires the companion ZIP-schema certificate (from the imported zip-schema module) to be inhabited, so the HDF5 sample sits on top of the already-checked archive layout.
Upstream lemmas are pure rfl or decide after unfolding the numeric defs: member name and posterior path by reflexivity; size positivity, object split, and count positivity by decidable arithmetic on the frozen naturals.
proof idea
Definitional structure instance. Each field of the certificate structure is assigned a previously proved local fact: member name via the reflexivity lemma on the frozen string; size positivity and uncompressed-greater-than-compressed via the corresponding decide lemmas; object-count split via the additive decide lemma; posterior path via reflexivity; posterior sample and field positivity via decide; and the ZIP-schema availability field via the upstream inhabited instance of the companion ZIP certificate. No new reasoning beyond field wiring.
why it matters
Gives a single named value that the one-line inhabitation theorem wraps as Nonempty of the certificate structure, which is the module's exportable "schema is checked" flag. Downstream reproducibility and verification layers can depend on that nonempty fact rather than on scattered numeric lemmas. In the Recognition Science verification stack this is structural hygiene only: it locks the layout of a real LIGO ringdown posterior file so later claims about rung placement or mass-ladder comparisons against GWTC-3 ringdown posteriors rest on an audited schema, not on an unchecked download. It does not itself touch the forcing chain (T5–T8), RCL, or the mass formula; it only anchors the external data contract those physics claims may later cite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.