IndisputableMonolith.Verification.GWTC3RingdownLikelihoodSelector

declarations in this module (17)

• def selectorTotalHDF5Files L47
• def selectorEligibleFiles L48
• def selectorBlockedFiles L49
• def selectorTotalModels L50
• def selectorEligibleModels L51
• def selectorBlockedModels L52
• def selectorNoMixedAggregation L53
• theorem selector_file_count_partition L57
• theorem selector_model_count_partition L62
• theorem selector_eligible_files_match_comparison L67
• theorem selector_total_files_match_taxonomy L70
• theorem selector_has_blocked_files L73
• theorem selector_no_mixed_aggregation_true L78
• structure GWTC3RingdownLikelihoodSelectorCert L83
• def gwtc3RingdownLikelihoodSelectorCert L101
• theorem gwtc3RingdownLikelihoodSelectorCert_inhabited L112
• theorem gwtc3_ringdown_likelihood_selector_one_statement L117