ConnectionCert
plain-language theorem explainer
ConnectionCert is a structure asserting that Christoffel symbols derived from any inverse metric and symmetric derivative tensor are symmetric in the lower indices, and that they vanish for the flat Minkowski metric with zero derivatives. A physicist formalizing GR in coordinate patches cites this to certify Levi-Civita properties without abstract manifolds. The declaration is a pure structure definition packaging the two fields with no computational content or proof obligations.
Claim. A structure whose fields are: (torsion_free) for any inverse metric $g^{-1}$ and derivative tensor $dg$ symmetric in its last two indices, the Christoffel symbols satisfy $Gamma^rho_{mu nu}=Gamma^rho_{nu mu}$; (flat_vanish) the symbols constructed from the Minkowski inverse metric and the zero derivative tensor are identically zero.
background
The module works in a 4-dimensional coordinate patch with Idx := Fin 4. InverseMetric is the structure holding a symmetric $g^{mu nu}$ satisfying the usual inverse relation. christoffel_from_metric builds $Gamma^rho_{mu nu} = (1/2) sum_sigma ginv(rho,sigma) (dg(mu,nu,sigma) + dg(nu,mu,sigma) - dg(sigma,mu,nu))$. The module doc states the goal is to formalize the Levi-Civita connection in coordinates while avoiding Mathlib's missing abstract manifold layer. Upstream, the flat_christoffel_vanish theorem records that symbols vanish on Minkowski space with constant metric.
proof idea
Structure definition with no body. The two fields directly reference christoffel_from_metric together with the symmetry assumption on dg and the explicit Minkowski case; no lemmas or tactics are invoked inside the declaration itself.
why it matters
Instantiated by the downstream theorem connection_cert, which supplies christoffel_symmetric to the torsion_free field and flat_christoffel_vanish to the flat_vanish field. The certificate therefore closes the local verification that the coordinate Christoffel symbols are torsion-free and flat, supporting the gravity module's coordinate-based treatment of the Levi-Civita connection. It sits outside the core Recognition Science forcing chain (T0-T8) and phi-ladder but supplies the GR infrastructure needed for later metric-compatibility arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.