delta
plain-language theorem explainer
The Kronecker delta on Fin n returns 1 precisely when its two indices coincide and 0 otherwise. Workers on affine connections and projective equivalence in n-dimensional cost spaces cite this selector to decompose Christoffel symbols. The definition is a direct case distinction on equality of the finite indices.
Claim. The Kronecker delta function on indices $i,j$ in a finite set of size $n$ is defined by $1$ if $i=j$ and $0$ otherwise.
background
The module records affine connections in $x$- and $t$-coordinates where $t= log x$. The $t$-coordinates are affine-flat by construction; their pullback to $x$-coordinates introduces the diagonal Christoffel term $-1/x_i$. The Kronecker delta appears inside the predicate ProjectivelyEquivalentToZeroAt, which declares a connection projectively equivalent to zero when there exists a vector field such that the Christoffel symbols decompose as the sum of two delta-weighted terms.
proof idea
One-line definition that returns 1 on equality of the two Fin n indices and 0 otherwise. No lemmas or tactics are applied; the body is the primitive case distinction used by all later index manipulations in the module.
why it matters
This supplies the index selector required by ProjectivelyEquivalentToZeroAt, which supports the one-dimensional equivalence theorem and the higher-dimensional non-equivalence theorem. Those results close the projective dichotomy for the pulled-back connection and feed the J-monotonicity certificates and derivative identities for J-cost. The construction is consistent with the framework requirement of D=3 spatial dimensions once n is specialized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.