IndisputableMonolith.Verification.GWTC3RingdownStatus

declarations in this module (16)

• def gwtc3AnalyzedEventCount L51
• def gwtc3FalseAlarmRateThreshold L54
• def gwtc3GravitonMassBound L57
• def gwtc3NoPostMergerEchoesReported L60
• def gwtc3NoSignificantGRDeviationReported L63
• def gwtc3QNMConsistentWithGR L66
• theorem gwtc3AnalyzedEventCount_pos L68
• theorem gwtc3FalseAlarmRateThreshold_pos L72
• theorem gwtc3GravitonMassBound_pos L77
• theorem gwtc3_echo_dataset_positive L84
• theorem gwtc3_qnm_dataset_positive L89
• theorem gwtc3_status_flags L94
• structure GWTC3RingdownStatusCert L102
• def gwtc3RingdownStatusCert L115
• theorem gwtc3RingdownStatusCert_inhabited L123
• theorem gwtc3_ringdown_status_one_statement L128