theorem proved term proof

`end_to_end`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 205theorem end_to_end (h_regge : ReggeConvergenceHypothesis) :
 206    EndToEndChain where
 207  bridge := bridge_certificate h_regge

proof body

Term-mode proof.

 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

depends on (6)

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
bridge_certificate in IndisputableMonolith.Relativity.Geometry.DiscreteBridge decl_use
EndToEndChain in IndisputableMonolith.Relativity.Geometry.DiscreteBridge decl_use
ReggeConvergenceHypothesis in IndisputableMonolith.Relativity.Geometry.DiscreteBridge decl_use
minkowski_tensor in IndisputableMonolith.Relativity.Geometry.Metric decl_use
curvature_axioms_hold in IndisputableMonolith.Relativity.Geometry.RiemannSymmetries decl_use