No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
236structure ParallelTransportCert (g : MetricTensor) : Prop where
237 flat_trivial : ∀ (γ : SpacetimeCurve) (V : ℝ → (Fin 4 → ℝ)),
238 g = minkowski_tensor → ParallelTransported g γ V →
239 ∀ lam μ, deriv (fun l => V l μ) lam = 0
240 inner_product_preserved : ∀ γ, ParallelTransportPreservesInnerProduct g γ
241
242/-- The parallel transport certificate holds for Minkowski. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (12)
Lean names referenced from this declaration's body.
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
MetricTensor
in IndisputableMonolith.Foundation.Hamiltonian
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
MetricTensor
in IndisputableMonolith.Gravity.Connection
decl_use
-
MetricTensor
in IndisputableMonolith.Meta.Homogenization
decl_use
-
MetricTensor
in IndisputableMonolith.Relativity.Geometry.Metric
decl_use
-
minkowski_tensor
in IndisputableMonolith.Relativity.Geometry.Metric
decl_use
-
ParallelTransported
in IndisputableMonolith.Relativity.Geometry.ParallelTransport
decl_use
-
ParallelTransportPreservesInnerProduct
in IndisputableMonolith.Relativity.Geometry.ParallelTransport
decl_use
-
SpacetimeCurve
in IndisputableMonolith.Relativity.Geometry.ParallelTransport
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use