kron
plain-language theorem explainer
The definition supplies the Kronecker delta on abstract tensor indices for use in ILG tensor expressions. Researchers handling symbolic index manipulations in the relativity sector of Recognition Science would cite this for metric and field operations. It is realized as a direct conditional definition that returns 1 on equal indices and 0 otherwise.
Claim. For indices $μ, ν$ drawn from the abstract index set $ℕ$, the Kronecker symbol is given by $δ_{μν} := 1$ if $μ = ν$ and $δ_{μν} := 0$ otherwise.
background
The module re-exports geometry and field types for ILG computations. The Index type is an abbreviation for natural numbers, serving as symbolic placeholders for tensor indices rather than concrete values. Upstream results include identity definitions from observer forcing and vantage categories, which establish canonical identity maps at minimum cost points.
proof idea
The declaration is a direct definition using a conditional expression on index equality.
why it matters
This definition anchors index notation in the ILG action module, enabling consistent treatment of raising and lowering operations in the Recognition framework. It supports the broader development of the action functional by providing the standard delta for contractions and metrics. No immediate downstream theorems are listed, leaving its integration into full tensor proofs as an open step in the relativity scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.