pith. machine review for the scientific record. sign in
theorem proved term proof

sparc_falsifier_cert

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

formal statement (Lean)

 186theorem sparc_falsifier_cert : SPARCFalsifierCert where
 187  zero_params := zero_free_params

proof body

Term-mode proof.

 188  params_from_phi := parameters_from_phi
 189  criterion_decidable := falsification_decidable
 190  global_only := global_only_policy
 191  ilg_beats_mond_mean := ilg_better_mean_than_mond
 192
 193end SPARCFalsifier
 194end Gravity
 195end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.