fundamental_theorem_existence
plain-language theorem explainer
The declaration states that every metric tensor admits a torsion-free metric-compatible connection given by the Christoffel symbols. A relativist would invoke it to justify the use of the Levi-Civita connection on any pseudo-Riemannian manifold. The proof is a term-mode assembly that directly inserts the two supporting lemmas into the FundamentalTheoremExistence structure.
Claim. For every metric tensor $g$, the associated Christoffel connection is torsion-free and metric-compatible, i.e., its torsion tensor vanishes and the covariant derivative of $g$ is zero.
background
The module establishes the fundamental theorem of pseudo-Riemannian geometry in local coordinates. A MetricTensor is a symmetric bilinear form on spacetime indices, serving as the local interface for the metric. The structure FundamentalTheoremExistence packages the two properties: IsTorsionFree for the Christoffel connection and the vanishing of cov_deriv_metric under the Koszul identity.
proof idea
The proof is a term-mode construction that populates the two fields of the FundamentalTheoremExistence structure. It applies levi_civita_torsion_free directly to obtain the torsion-free property and uses metric_compatible_of_koszul to satisfy the metric-compatibility condition for every point x satisfying the Koszul identity.
why it matters
This theorem supplies the existence half of the Fundamental Theorem, which is consumed by levi_civita_certificate to produce the full LeviCivitaCertificate and by bridge_certificate to certify the discrete-to-continuum bridge under the Regge hypothesis. It reproduces the classical result from Wald and do Carmo that every pseudo-Riemannian metric determines a unique torsion-free metric-compatible connection, here realized via the Christoffel symbols of Curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.