 121
 122/-! ## Certificate -/
 123
 124structure ConnectionCert where
 125  torsion_free : ∀ (ginv : InverseMetric) (dg : Idx → Idx → Idx → ℝ),
 126    (∀ mu nu sigma, dg mu nu sigma = dg mu sigma nu) →
 127    ∀ rho mu nu,
 128      (christoffel_from_metric ginv dg).gamma rho mu nu =
 129      (christoffel_from_metric ginv dg).gamma rho nu mu
 130  flat_vanish : ∀ rho mu nu : Idx,
 131    (christoffel_from_metric minkowski_inverse (fun _ _ _ => 0)).gamma rho mu nu = 0
 132
 133theorem connection_cert : ConnectionCert where
 134  torsion_free := christoffel_symmetric
 135  flat_vanish := flat_christoffel_vanish
 136
 137end Connection
 138end Gravity
 139end IndisputableMonolith

papers checked against this theorem

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