`end_to_end`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Geometry.DiscreteBridge
domain: Relativity
line: 205 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Geometry.DiscreteBridge on GitHub at line 205.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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.