Verification Gwtc3 Ringdown Zip Schema

The ZIP schema check

A ZIP file is a container that stores files in a compressed format, and its central directory is an index at the end of the file that lists every entry, its location, and its size. Verification of the GWTC-3 ringdown ZIP schema is the process of checking that this index for a specific public data file, IGWN-GWTC3-TGR-v1-rin.zip, is internally consistent and complete. The file in question is a 1,444,203,951 byte archive containing gravitational-wave ringdown data from the third observing run of the LIGO-Virgo-KAGRA collaboration.

The framework's machine-checked library of formal theorems establishes a structural certificate for this archive. The central directory, which starts at byte offset 1,444,176,371 and occupies 27,558 bytes, lists exactly 244 entries. Of these, 243 are HDF5 data files and one is a directory marker, all sharing the top-level prefix rin. The certificate proves basic consistency facts: the entry count is positive, the extension counts sum to the total, all entries share the top-level prefix, the total uncompressed size (1,963,931,876 bytes) exceeds the compressed size (1,444,151,741 bytes), and the central directory itself lies entirely within the source file.

What this establishes in plain language is that the archive's structure is exactly what the framework's manifest expects, with zero errors and zero unproven assumptions. The verification was performed by fetching only the central directory via an HTTP range request, avoiding a full 1.44 gigabyte download. The single-statement theorem gwtc3_ringdown_zip_schema_one_statement bundles all these facts into one machine-checked assertion, and the certificate structure GWTC3RingdownZipSchemaCert packages them as a reusable proof object.

This is schema inspection only, not an analysis of the gravitational-wave signals themselves. The verification does not compute posterior likelihoods or validate the physics content of the HDF5 files. What it does provide is a verified foundation: before any scientific analysis of the ringdown data can be trusted, the integrity of the data container itself must be established. This closes that gap with a formal, machine-checked guarantee that the archive is structurally sound, so subsequent analysis can proceed without re-checking the container layer.

/-- One-statement schema theorem for the ringdown ZIP. -/
theorem gwtc3_ringdown_zip_schema_one_statement :
    (ringdownZipEntryCount = 244) ∧
    (ringdownZipH5Count = 243) ∧
    (ringdownZipDirectoryMarkerCount = 1) ∧
    (ringdownZipH5Count + ringdownZipDirectoryMarkerCount = ringdownZipEntryCount) ∧
    (ringdownZipTopLevelRinCount = ringdownZipEntryCount) ∧
    (ringdownZipTotalCompressedSize < ringdownZipTotalUncompressedSize) ∧
    (ringdownFile.key = "IGWN-GWTC3-TGR-v1-rin.zip") ∧
    Nonempty GWTC3RingdownZipSchemaCert :=
  ⟨rfl, rfl, rfl,
   ringdown_zip_extension_count_sum,
   ringdown_zip_top_level_count_eq_entries,
   ringdown_zip_total_uncompressed_gt_compressed,
   ringdown_file_key,
   gwtc3RingdownZipSchemaCert_inhabited⟩

theorem ringdown_zip_total_uncompressed_gt_compressed :
    ringdownZipTotalCompressedSize < ringdownZipTotalUncompressedSize := by
  unfold ringdownZipTotalCompressedSize ringdownZipTotalUncompressedSize
  decide

theorem ringdown_zip_cd_inside_source :
    ringdownZipCentralDirectoryOffset + ringdownZipCentralDirectorySize <
      ringdownZipSourceSizeBytes := by
  unfold ringdownZipCentralDirectoryOffset ringdownZipCentralDirectorySize
    ringdownZipSourceSizeBytes
  decide

What this page does not claim

This verification does not analyze the gravitational-wave signals or compute any posterior likelihoods. This verification does not confirm the scientific validity of the data, only the structural integrity of the ZIP container. The framework does not claim to have downloaded or inspected the full 1.44 gigabyte payload.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/GWTC3RingdownZipSchema.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: