levi_civita_certificate
plain-language theorem explainer
Every metric tensor admits a unique torsion-free metric-compatible connection. General relativists cite this when deriving Christoffel symbols or the geodesic equation from the metric alone. The proof is a term construction that directly supplies the existence and uniqueness fields of the certificate structure from the two fundamental theorems.
Claim. For any metric tensor $g$, there exists a torsion-free metric-compatible affine connection, and any such connection is unique.
background
The module establishes the Fundamental Theorem of Pseudo-Riemannian Geometry: on any pseudo-Riemannian manifold $(M,g)$ there exists a unique torsion-free, metric-compatible connection whose coefficients are the Christoffel symbols. A MetricTensor is a symmetric bilinear form on spacetime indices (Fin 4), appearing in multiple local interfaces across Hamiltonian, Gravity, and Homogenization modules. The upstream fundamental_theorem_existence supplies torsion_free via levi_civita_torsion_free and metric_compatible via metric_compatible_of_koszul; fundamental_theorem_uniqueness supplies the uniqueness clause via connection_uniqueness_lowered.
proof idea
Term proof that constructs the LeviCivitaCertificate structure by direct field assignment: existence is set to the result of fundamental_theorem_existence g, and uniqueness is set to the result of fundamental_theorem_uniqueness g.
why it matters
This declaration packages the existence and uniqueness results into the single LeviCivitaCertificate structure, completing the Fundamental Theorem of Pseudo-Riemannian Geometry as stated in the module doc (Wald Theorem 3.1.1, do Carmo Theorem 2.3). It supplies the geometric foundation used by downstream curvature and derivative modules in the Relativity section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.