pith. machine review for the scientific record. sign in
def definition def or abbrev high

christoffel

show as:
view Lean formalization →

The definition supplies the standard coordinate formula for the Levi-Civita connection coefficients of a general four-dimensional metric tensor. Researchers building geodesic equations or curvature tensors inside the Recognition relativity module cite it when passing from the metric to covariant derivatives. The body is a direct transcription of the classical expression that contracts the inverse metric against three partial derivatives of the metric components.

claimThe Christoffel symbols associated to a metric tensor $g$ are the functions $x,rho,mu,nu mapsto frac12 g^{rho lambda}(x) bigl( partial_mu g_{nu lambda}(x) + partial_nu g_{mu lambda}(x) - partial_lambda g_{mu nu}(x) bigr)$, where the inverse metric and partial derivatives are taken with respect to the coordinate chart on $mathbb R^4$.

background

The module Relativity.Geometry.Curvature works inside the Recognition framework's four-dimensional spacetime setting. The structure MetricTensor from Foundation.Hamiltonian supplies a local bilinear form whose components are accessed by a function of type (Fin 4 to R) to (Fin 4 to R) to (Fin 2 to Fin 4) to R. The accessor inverse_metric and the operator partialDeriv_v2 are imported as placeholders that allow the formula to be written without fixing a concrete metric at this stage.

proof idea

The definition is the explicit coordinate formula for the Christoffel symbols of the second kind. It applies inverse_metric to contract the sum over the dummy index lambda with the combination of three partialDeriv_v2 terms that implement the standard expression partial_mu g_nu lambda plus partial_nu g_mu lambda minus partial_lambda g_mu nu. No lemmas are invoked; the body is the direct transcription of the classical formula.

why it matters in Recognition Science

This definition supplies the connection coefficients required by the covariant derivative in CovariantDerivative.cov_deriv_1_2 and by the Riemann tensor construction in the same module. It is used to prove symmetry of the Christoffel symbols and to show that they vanish for the Minkowski metric. In the broader framework it bridges the metric structure introduced in Foundation.Hamiltonian to the curvature computations needed for the Einstein tensor and geodesic motion in the Action.EulerLagrange module.

scope and limits

formal statement (Lean)

  13noncomputable def christoffel (g : MetricTensor) : (Fin 4 → ℝ) → Fin 4 → Fin 4 → Fin 4 → ℝ :=

proof body

Definition body.

  14  fun x rho mu nu =>
  15    (1/2 : ℝ) * Finset.univ.sum (fun (lambda : Fin 4) =>
  16      (inverse_metric g) x (fun _ => rho) (fun _ => lambda) * (
  17        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then mu else lambda)) nu x) +
  18        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then nu else lambda)) mu x) -
  19        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then mu else nu)) lambda x)
  20      ))
  21
  22/-- Christoffel symbols are symmetric in the lower indices (torsion-free). -/

used by (30)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.