IndisputableMonolith.Verification.GWTC3RingdownFilenameTaxonomy

declarations in this module (25)

• def taxonomyHDF5FileCount L41
• def taxonomyEventCount L42
• def taxonomyPyringCount L43
• def taxonomyPSEOBNRv4HMCount L44
• def taxonomyKerrCount L45
• def taxonomyMMRDNPCount L46
• def taxonomyDampedSinusoidCount L47
• def taxonomyWaveformCount L48
• def taxonomyTotalCompressedSize L49
• def taxonomyTotalUncompressedSize L50
• def taxonomySmallestMember L51
• def taxonomyLargestMember L52
• theorem taxonomy_pipeline_sum L56
• theorem taxonomy_category_sum L61
• theorem taxonomy_hdf5_count_matches_zip_schema L68
• theorem taxonomy_total_compressed_matches_zip_schema L71
• theorem taxonomy_total_uncompressed_matches_zip_schema L74
• theorem taxonomy_uncompressed_gt_compressed L77
• theorem taxonomy_event_count_pos L82
• theorem taxonomy_smallest_member_named L86
• theorem taxonomy_largest_member_named L89
• structure GWTC3RingdownFilenameTaxonomyCert L94
• def gwtc3RingdownFilenameTaxonomyCert L110
• theorem gwtc3RingdownFilenameTaxonomyCert_inhabited L123
• theorem gwtc3_ringdown_filename_taxonomy_one_statement L128