 175
 176/-! ## Certificate -/
 177
 178structure SPARCFalsifierCert where
 179  zero_params : per_galaxy_free_parameters = 0
 180  params_from_phi : alpha_locked = (1 - 1/phi) / 2 ∧ upsilon_locked = phi ∧
 181    clag_locked = phi ^ (-(5 : ℝ))
 182  criterion_decidable : ∀ x : ℝ, ILG_falsified x ∨ ILG_passes x
 183  global_only : GlobalOnlyPolicy
 184  ilg_beats_mond_mean : paper2_mean_chi2 < mond_mean_chi2
 185
 186theorem sparc_falsifier_cert : SPARCFalsifierCert where
 187  zero_params := zero_free_params
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.