kronecker_symm
plain-language theorem explainer
The Kronecker delta is symmetric under index swap by its piecewise definition. Researchers manipulating tensor expressions in relativity would cite this when reordering indices in contractions or metric raisings. The proof applies case analysis on index equality, with immediate simplification in the equal branch and a symmetric inequality derivation in the unequal branch.
Claim. For any natural number $n$ and indices $μ, ν ∈ Fin n$, the Kronecker delta satisfies $δ_{μν} = δ_{νμ}$.
background
The Kronecker delta is defined to return 1 on equal indices and 0 otherwise. This module supplies placeholder manifold types, points, tangent vectors, covectors, and spacetime indices to support typed relativity calculations, but the entire file is marked as a scaffold outside the verified certificate chain. The symmetry result depends only on the upstream definition of the Kronecker delta.
proof idea
The tactic proof opens with case analysis on whether μ equals ν. The equal case simplifies directly via the definition. The unequal case first derives ν ≠ μ by symmetry of equality, then simplifies in both branches using the definition.
why it matters
This supplies the elementary symmetry needed for consistent index algebra in the relativity geometry scaffold. No downstream theorems yet depend on it, and the module itself lies outside the verified RS chain and forcing sequence. It fills a basic placeholder role rather than advancing any T0-T8 step or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.