 195
 196    The five hypotheses are all standard external mathematics or physics,
 197    not RS-specific assumptions. -/
 198structure EndToEndChain : Prop where
 199  bridge : DiscreteContinuumBridge
 200  curvature_axioms : ∀ x,
 201    (∀ ρ σ μ ν, riemann_lowered_eq_explicit_hypothesis minkowski_tensor x ρ σ μ ν) →
 202    (∀ μ ν, riemann_trace_vanishes_hypothesis minkowski_tensor x μ ν) →
 203    CurvatureAxiomsHold minkowski_tensor x
 204
 205theorem end_to_end (h_regge : ReggeConvergenceHypothesis) :
 206    EndToEndChain where
 207  bridge := bridge_certificate h_regge
 208  curvature_axioms := fun x h_eq h_trace => curvature_axioms_hold minkowski_tensor x h_eq h_trace
 209
 210end -- noncomputable section
 211
 212end Geometry
 213end Relativity
 214end IndisputableMonolith

papers checked against this theorem

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