IndisputableMonolith.Verification.GWTC3RingdownGuardedFamilyScripts

declarations in this module (15)

• def guardedScriptCount L41
• def smokeTestCount L42
• def smokePassCount L43
• def smokeAllPassed L44
• theorem guarded_script_count_matches_selector L46
• theorem smoke_all_passed L49
• theorem smoke_pass_count_eq_test_count L51
• theorem guarded_DS_script_accepted L56
• theorem guarded_Kerr2200_script_accepted L60
• theorem guarded_Kerr22010_script_accepted L64
• theorem representative_blocked_rejected L68
• structure GWTC3RingdownGuardedFamilyScriptsCert L76
• def gwtc3RingdownGuardedFamilyScriptsCert L102
• theorem gwtc3RingdownGuardedFamilyScriptsCert_inhabited L116
• theorem gwtc3_ringdown_guarded_family_scripts_one_statement L121