ChristoffelSymmetric
plain-language theorem explainer
Defines the predicate requiring Christoffel symbols to be symmetric under interchange of the lower indices. Workers verifying metric-induced connections cite it to confirm the torsion-free property. The body is a direct universal quantification over spacetime points and index triples with no auxiliary lemmas.
Claim. Let $cs$ be a Christoffel symbol bundle. The predicate holds when $cs.Γ(x,ρ,μ,ν)=cs.Γ(x,ρ,ν,μ)$ for every point $x$ and indices $ρ,μ,ν$.
background
The module supplies placeholder definitions for relativity geometry. The structure ChristoffelSymbols packages a map $Γ$ from spacetime points (Fin 4 → ℝ) and three indices to reals, defaulting to zero at every entry. Module documentation states these are structural placeholders, not rigorous differential geometry, and should not be cited as proven mathematics.
proof idea
Direct definition. The body states the equality $cs.Γ x ρ μ ν = cs.Γ x ρ ν μ$ as a universal quantifier over $x,ρ,μ,ν$. No lemmas or tactics are invoked beyond the quantified statement itself.
why it matters
Supplies the target property for the downstream lemma christoffel_from_metric_symmetric, which shows symbols derived from a metric tensor obey the symmetry. This mirrors the classical torsion-free character of the Levi-Civita connection. The entry remains a placeholder outside the main certificate chain and does not link to the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.