ConnectionCert
plain-language theorem explainer
ConnectionCert packages two properties of the Levi-Civita connection in local coordinates: the Christoffel symbols derived from any inverse metric and its derivatives are symmetric in the lower indices when those derivatives are symmetric, and the symbols vanish identically for the Minkowski metric with zero derivatives. Formalizers of general relativity inside the Recognition Science framework cite it to certify that the coordinate connection meets the torsion-free and flat-space requirements before building curvature or geodesic results. The
Claim. A structure whose fields assert: (i) for any inverse metric $g^{rho sigma}$ and partial derivatives $partial_mu g_{nu sigma}$, symmetry of the derivatives in the last two indices implies symmetry of the Christoffel symbols $Gamma^rho_{mu nu} = Gamma^rho_{nu mu}$; (ii) the Christoffel symbols constructed from the Minkowski inverse metric and the zero derivative function vanish for all index triples.
background
The Gravity.Connection module works in a local coordinate patch on 4-dimensional spacetime, with indices drawn from Fin 4. InverseMetric is the structure holding a symmetric map $g^{mu nu}$ that contracts with the metric to the Kronecker delta. The function christoffel_from_metric builds the standard Levi-Civita expression $Gamma^rho_{mu nu} = (1/2) g^{rho sigma} (partial_mu g_{nu sigma} + partial_nu g_{mu sigma} - partial_sigma g_{mu nu})$ from an InverseMetric and a derivative tensor dg.
proof idea
ConnectionCert is a structure definition whose two fields directly state the required properties. No lemmas are invoked and no tactics are executed; the declaration simply records the torsion-free condition under the symmetry hypothesis on dg and the explicit vanishing statement for the Minkowski case.
why it matters
The structure is instantiated by the theorem connection_cert, which supplies the torsion-free field from christoffel_symmetric and the flat-vanishing field from flat_christoffel_vanish. It anchors the coordinate treatment of the Levi-Civita connection inside the Recognition Science gravity development, confirming consistency with the flat-space limit before curvature or geodesic constructions proceed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.