IndisputableMonolith.Verification.GWTC3RingdownZipSchema

declarations in this module (20)

• def ringdownZipSourceSizeBytes L40
• def ringdownZipCentralDirectoryOffset L41
• def ringdownZipCentralDirectorySize L42
• def ringdownZipEntryCount L43
• def ringdownZipH5Count L44
• def ringdownZipDirectoryMarkerCount L45
• def ringdownZipTopLevelRinCount L46
• def ringdownZipTotalCompressedSize L47
• def ringdownZipTotalUncompressedSize L48
• theorem ringdown_zip_source_size_pos L52
• theorem ringdown_zip_cd_size_pos L56
• theorem ringdown_zip_entry_count_pos L60
• theorem ringdown_zip_extension_count_sum L64
• theorem ringdown_zip_top_level_count_eq_entries L69
• theorem ringdown_zip_total_uncompressed_gt_compressed L74
• theorem ringdown_zip_cd_inside_source L79
• structure GWTC3RingdownZipSchemaCert L88
• def gwtc3RingdownZipSchemaCert L104
• theorem gwtc3RingdownZipSchemaCert_inhabited L114
• theorem gwtc3_ringdown_zip_schema_one_statement L119