module module high

`IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSchema`

Records the fixed HDF5 layout of one GWTC-3 ringdown posterior file drawn from the IGWN ringdown ZIP: member path, compressed and uncompressed sizes, header and data offsets, object/group/dataset counts, and the posterior-samples dataset path and field counts. Verification authors cite it when binding range-read bytes to a named schema. The module is a structural constant package, not a derived inequality.

claimThe module fixes a single GWTC-3 ringdown HDF5 sample schema: member name, compressed size $C$, uncompressed size $U$, local-header offset $h$, data offset $d$, HDF5 object/group/dataset/root-attribute counts, posterior-samples dataset path, sample count $N$, and field count $F$, as extracted from the IGWN ringdown archive.

background

Recognition Science verification against LIGO/Virgo/KAGRA ringdown posteriors needs machine-checkable bindings to public IGWN releases, not hand-copied tables. The upstream ZIP schema module already pins the central directory of IGWN-GWTC3-TGR-v1-rin.zip via HTTP range request (directory only, no full 1.44 GB download).

This module steps one level deeper: it names the concrete HDF5 member used as the sample (a single-mode pyring posterior file) and records the structural integers that any honest range-read of that member must reproduce. Sibling constants cover ZIP-level sizes and offsets plus HDF5 inventory (objects, groups, datasets, root attributes) and the posterior-samples path with its row and field counts.

The setting is pure structural verification: equality of published archive metadata to Lean constants, with zero RS-internal axioms claimed in the neighboring summary module.

proof idea

Definition and constant module, not a multi-step proof development. It packages named numeric and string literals (member path, sizes, offsets, HDF5 inventory counts, posterior dataset path and dimensions) that match the range-read sample. Downstream summary theorems import these constants and assert the extracted posterior statistics against them. No tactic script beyond whatever trivial rfl/definitional equalities close the one-statement schema claim.

why it matters in Recognition Science

Feeds GWTC3RingdownHDF5SampleSummary, which records the first posterior-summary statistics from the range-read member rin/rin_S190727h_pyring_DS_1mode_10M.h5 and is marked a structural theorem (0 sorry, 0 RS-internal axiom). Without a frozen sample schema, those summary equalities would float free of the public archive layout.

In the broader Verification domain this is infrastructure for confronting RS mass/ladder and ringdown predictions with GWTC-3 releases: the ZIP schema pins the container; this module pins the HDF5 interior of one canonical member; the summary module then exposes the numerical posterior content. It does not itself derive a physics constant, but it is the schema hinge those checks hang on.

scope and limits

Does not prove correctness of the full 1.44 GB ZIP payload, only the named sample member schema.
Does not extract or certify posterior means, variances, or credible intervals.
Does not claim the sample event is preferred by Recognition Science dynamics.
Does not generalize automatically to other GWTC-3 ringdown HDF5 members.
Does not replace IGWN data-release authority; it freezes one observed layout.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownZipSchema module_import

declarations in this module (23)

def sampleMemberName L51
def sampleCompressedSize L52
def sampleUncompressedSize L53
def sampleLocalHeaderOffset L54
def sampleDataOffset L55
def sampleHDF5ObjectCount L56
def sampleGroupCount L57
def sampleDatasetCount L58
def sampleRootAttrCount L59
def posteriorSamplesDatasetPath L60
def posteriorSamplesCount L61
def posteriorFieldCount L62
theorem sample_sizes_pos L66
theorem sample_uncompressed_gt_compressed L71
theorem sample_object_count_split L76
theorem sample_posterior_samples_nonempty L81
theorem sample_posterior_field_count_pos L86
theorem sample_member_is_h5 L91
theorem sample_posterior_dataset_named L94
structure GWTC3RingdownHDF5SampleSchemaCert L99
def gwtc3RingdownHDF5SampleSchemaCert L117
theorem gwtc3RingdownHDF5SampleSchemaCert_inhabited L128
theorem gwtc3_ringdown_hdf5_sample_schema_one_statement L133