kron
plain-language theorem explainer
Kronecker delta on Fin 4: 1 on the diagonal, 0 off it. Local copy used throughout the Lorentzian edge TT layer so projector algebra and double sums collapse to matrix entries. Citation target for anyone expanding null mixed projectors or proving sum-selection identities against a Minkowski wave covector. Body is the standard piecewise definition.
Claim. For indices $i,j\in\{0,1,2,3\}$, define $\delta_{ij}\in\mathbb{R}$ by $\delta_{ij}=1$ if $i=j$ and $\delta_{ij}=0$ otherwise.
background
This module is the Lorentzian algebraic layer of the edge transverse-traceless decomposition campaign (Wave 4 / W4-1). It treats symmetric real $4\times 4$ matrices against a Minkowski wave covector on $\mathrm{Fin},4$, signature $(-+++)$, including the null case with an auxiliary null covector $\ell$.
Index raising negates the time component; the Minkowski pairing and metric-trace are the usual $\eta$-contractions. Lorentz transversality contracts the second index of $H$ against the raised wave covector. Non-null and null projectors are built from $\eta$ and outer products of the wave data.
The upstream ILG action already defines a symbolic Kronecker $\delta_{\mu\nu}$ on a generic index type. This local definition specializes that pattern to $\mathrm{Fin},4$ so every subsequent sum over projector factors can select matrix entries without leaving the module.
proof idea
Pure definition: the real-valued piecewise map that returns $1$ when the two $\mathrm{Fin},4$ arguments are equal and $0$ otherwise. No lemmas are applied; downstream proofs unfold it and invoke Finset.sum_eq_single (or simp) to kill off-diagonal terms.
why it matters
Every algebraic identity that expands a null mixed projector $P_i{}^a=\delta_i{}^a-S_i{}^a$ or collapses a double sum against $H_{ab}$ begins from this delta. Downstream consumers include nullPMixed (the mixed projector itself), nullPhp_expand_algebra (four-term expansion of $(PHP)_{ij}$), and the selection lemmas sum_kron_left, sum_kron_right, sum_kron_H_kron, sum_kron_H_S, plus the raised-index variants.
Those identities are the linear-algebra engine of the Lorentzian TT layer. The module explicitly does not yet decompose Regge edge perturbations, prove continuum EH recovery, or attach polarization normalizations; this delta is the elementary selector that makes the algebraic bookkeeping kernel-checkable inside that scoped campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.