module
module
IndisputableMonolith.Verification.FalsifierLikelihoodRegister
show as:
view Lean formalization →
used by (1)
depends on (8)
-
IndisputableMonolith.Verification.CassiniStrongFieldLikelihood -
IndisputableMonolith.Verification.DarkEnergyWPlanckLikelihood -
IndisputableMonolith.Verification.EHTM87StrongFieldLikelihood -
IndisputableMonolith.Verification.EPTAPTALikelihood -
IndisputableMonolith.Verification.GravityS2StrongFieldLikelihood -
IndisputableMonolith.Verification.GWTC3RingdownStatus -
IndisputableMonolith.Verification.NANOGravPTALikelihood -
IndisputableMonolith.Verification.OmegaLambdaPlanckLikelihood
declarations in this module (10)
-
def
totalFalsifierRows -
def
rowsWithLikelihoodOrStatus -
def
datasetOnlyRows -
def
individualLikelihoodArtifacts -
theorem
row_coverage_arithmetic -
theorem
individual_artifact_count_pos -
structure
FalsifierLikelihoodRegisterCert -
def
falsifierLikelihoodRegisterCert -
theorem
falsifierLikelihoodRegisterCert_inhabited -
theorem
falsifier_likelihood_register_one_statement