christoffel_from_metric_symmetric
plain-language theorem explainer
The lemma establishes symmetry of the lower indices in Christoffel symbols constructed from a metric tensor. It would be cited when setting up the torsion-free Levi-Civita connection in placeholder relativity geometry within Recognition Science. The proof is a direct reduction that unfolds the symmetry predicate and the metric construction, then confirms equality by reflexivity on the indices.
Claim. Let $g$ be a metric tensor. Let $Γ$ denote the Christoffel symbols constructed from $g$ via the standard formula involving the inverse metric and metric derivatives. Then $Γ^ρ_{μν} = Γ^ρ_{νμ}$ holds for all indices $ρ, μ, ν$ and points $x$.
background
This declaration sits in a scaffold module that supplies placeholder definitions for Christoffel symbols and covariant derivatives; the module documentation states explicitly that all symbols default to zero and that the content is not part of the verified certificate chain. ChristoffelSymmetric is the predicate asserting $Γ^ρ_{μν} = Γ^ρ_{νμ}$ for the symbol object. The upstream construction christoffel_from_metric (imported from Gravity.Connection) builds the symbols by the usual expression $(1/2) g^{ρσ} (∂μ g{νσ} + ∂ν g{μσ} - ∂σ g{μν})$ using an inverse-metric interface and derivative tensor. MetricTensor itself is the local bilinear-form structure that defaults to the zero form in the sealed build. Upstream structures such as MetricTensor and the various forcing-derived objects calibrate the geometric layer to the J-cost and phi-ladder conventions of the foundation.
proof idea
The term-mode proof unfolds ChristoffelSymmetric and christoffel_from_metric, introduces the four indices, and applies reflexivity; the equality holds identically once the definitions are expanded because the placeholder construction is symmetric by fiat.
why it matters
The lemma secures the lower-index symmetry required for any torsion-free connection in the placeholder relativity geometry. It feeds the sibling declarations on covariant derivatives and metric compatibility, though the used-by count is currently zero and the module is marked outside the certificate chain. It therefore touches the open question of how the geometric layer will eventually be linked to the core forcing chain (T0–T8) and Recognition Composition Law without introducing non-zero curvature or non-trivial J-cost defects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.