module module

`IndisputableMonolith.Verification.GWTC3RingdownFamilyGuard`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Verification.GWTC3RingdownGuardedFamilyScripts module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownLikelihoodSelector module_import

declarations in this module (23)

inductive GuardDecision L40
def guardModel L45
theorem guard_accepts_DS L51
theorem guard_accepts_Kerr2200 L56
theorem guard_accepts_Kerr22010 L61
theorem guard_rejects_Kerr2210 L66
theorem guard_rejects_Kerr221Domega L71
theorem guard_rejects_MMRDNP L76
theorem guard_rejects_pseobnrv4hm L81
theorem guard_rejects_unknown L86
def guardEligibleModelCount L93
def guardBlockedModelCount L94
def guardTestCount L95
def guardAcceptedTestCount L96
def guardRejectedTestCount L97
def guardAllTestsPassed L98
theorem guard_counts_match_selector L100
theorem guard_test_count_partition L106
theorem guard_all_tests_passed L111
structure GWTC3RingdownFamilyGuardCert L116
def gwtc3RingdownFamilyGuardCert L132
theorem gwtc3RingdownFamilyGuardCert_inhabited L146
theorem gwtc3_ringdown_family_guard_one_statement L151