ConnectionCert
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
claimA 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 in Recognition Science
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.
scope and limits
- Does not establish a global manifold or atlas.
- Does not compute Christoffel symbols for non-constant metrics.
- Does not derive the Riemann tensor or geodesic deviation.
- Does not invoke Recognition Science constants such as phi or the J-cost function.
formal statement (Lean)
124structure ConnectionCert where
125 torsion_free : ∀ (ginv : InverseMetric) (dg : Idx → Idx → Idx → ℝ),
126 (∀ mu nu sigma, dg mu nu sigma = dg mu sigma nu) →
127 ∀ rho mu nu,
128 (christoffel_from_metric ginv dg).gamma rho mu nu =
129 (christoffel_from_metric ginv dg).gamma rho nu mu
130 flat_vanish : ∀ rho mu nu : Idx,
131 (christoffel_from_metric minkowski_inverse (fun _ _ _ => 0)).gamma rho mu nu = 0
132