IndisputableMonolith.Verification.GWTC3RingdownSharedRunner

declarations in this module (13)

• def sharedRunnerPresent L38
• def refactoredFamilyScriptCount L39
• def supportedMappingCount L40
• def smokeTestsAfterRefactor L41
• def smokePassesAfterRefactor L42
• theorem shared_runner_present L44
• theorem refactored_count_matches_guarded_count L46
• theorem supported_mapping_count_pos L49
• theorem smoke_after_refactor_all_passed L54
• structure GWTC3RingdownSharedRunnerCert L59
• def gwtc3RingdownSharedRunnerCert L70
• theorem gwtc3RingdownSharedRunnerCert_inhabited L77
• theorem gwtc3_ringdown_shared_runner_one_statement L82