connection_cert
plain-language theorem explainer
The connection_cert theorem constructs a certificate verifying that Christoffel symbols from the metric are torsion-free under derivative symmetry and vanish for the constant Minkowski metric. Coordinate-based general relativity work would cite it to confirm Levi-Civita properties in local patches without abstract manifolds. The proof is a direct term construction that populates the two fields of the ConnectionCert structure from the symmetry and flat-vanishing lemmas.
Claim. The Christoffel symbols derived from an inverse metric and its first derivatives satisfy symmetry in the lower indices whenever the derivatives obey the metric symmetry condition, and they vanish identically for the constant Minkowski metric.
background
The module works in local coordinates on R^4 with the metric as a smooth matrix-valued function g, avoiding the Mathlib abstract manifold gap. MetricTensor denotes the symmetric nondegenerate bilinear form g_mu nu, while christoffel_from_metric encodes the standard formula Gamma^rho_mu nu = (1/2) g^rho sigma (partial_mu g_nu sigma + partial_nu g_mu sigma - partial_sigma g_mu nu). The ConnectionCert structure packages the two required properties: torsion-freeness under the assumption that metric derivatives satisfy dg mu nu sigma = dg mu sigma nu, and flat vanishing for the Minkowski case.
proof idea
The proof is a term-mode construction of the ConnectionCert structure. It supplies the torsion_free field by direct reference to the christoffel_symmetric lemma and the flat_vanish field by direct reference to the flat_christoffel_vanish lemma.
why it matters
This declaration completes the basic certification of the Levi-Civita connection inside the Gravity.Connection module, supplying the torsion-free and flat properties needed before curvature or geodesic computations. It supports the Recognition Science coordinate-patch approach to gravity, consistent with the eight-tick octave and D=3 spatial dimensions embedded in 4D spacetime. No open questions are closed here, but the result finishes the local connection axioms in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.