kronecker_diag
plain-language theorem explainer
The declaration establishes that the Kronecker delta equals one whenever both indices coincide. It would be referenced in tensor index contractions or diagonal simplifications inside the manifold placeholder. The proof is a one-line wrapper that applies simplification directly to the definition.
Claim. For any natural number $n$ and index $μ$ in the finite set of size $n$, the Kronecker delta satisfies $δ_{μμ}=1$.
background
The module supplies a minimal typed manifold structure for relativity geometry, explicitly labeled a scaffold that is not part of the verified certificate chain. The upstream definition states that the Kronecker delta returns 1 when the two indices are equal and 0 otherwise. This supplies the standard diagonal property needed for index algebra in coordinate charts.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of kronecker, which reduces the equality by case analysis on whether the indices match.
why it matters
The identity supplies the basic diagonal case for the Kronecker delta inside the scaffold manifold infrastructure. No downstream theorems are recorded, consistent with the module's placeholder status outside the main Recognition Science forcing chain. It fills a routine algebraic slot rather than advancing any T0-T8 step or RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.