kronecker_off_diag
plain-language theorem explainer
The declaration states that the Kronecker delta on indices from a finite set of size n equals zero whenever the indices differ. It would be invoked in coordinate-basis calculations on the manifold to drop off-diagonal contributions. The proof is a one-line simplification that unfolds the definition of kronecker and applies the supplied inequality.
Claim. Let $n$ be a natural number and let $μ, ν$ be elements of the finite set with $n$ elements. If $μ ≠ ν$, then the Kronecker delta $δ_{μν}$ equals 0.
background
The module supplies placeholder type definitions for manifold objects (points, tangent vectors, covectors, spacetime indices via Fin n) to support relativity geometry infrastructure. The Kronecker delta itself is introduced by the sibling definition kronecker as the function that returns 1 when its two Fin n arguments are equal and 0 otherwise. The module documentation explicitly labels the entire file a scaffold that is not part of the verified certificate chain and warns against citing its contents as rigorous mathematics. Upstream structures supply context on J-cost convexity, spectral emergence of gauge groups, and nuclear density tiers, but none of these are invoked by the present theorem.
proof idea
The proof is a one-line wrapper that invokes the simp tactic on the definition of kronecker together with the hypothesis that the indices are unequal, which reduces the expression directly to 0 by the if-then-else case in the definition.
why it matters
The result supplies an elementary index identity used in any tensor manipulation that relies on the Kronecker delta within the manifold layer. It stands next to the sibling declarations kronecker_symm and kronecker_diag. Because the module is declared a scaffold outside the certificate chain, the theorem does not feed any downstream verified result and does not close any step in the T0-T8 forcing chain or the Recognition Composition Law. It merely supports placeholder index arithmetic in a setting that ultimately aims at D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.