tPulledConnection_offDiag
plain-language theorem explainer
The off-diagonal coefficients of the pulled-back flat connection vanish identically. Researchers examining affine structures in logarithmic coordinates cite this when confirming the explicit Christoffel form. The argument unfolds the piecewise definition and simplifies directly from the index inequality.
Claim. Let $tPulledConnection(x; i,j,k)$ denote the coefficient of the flat $t$-connection pulled back via $t_m = log x_m$. Then $tPulledConnection(x; i,j,k) = 0$ whenever it is not the case that $i = j = k$.
background
The module records affine connections in $x$- and $t$-coordinates, where the $t = log x$ coordinates are affine-flat by construction. The type $Vec n$ is the space of $n$-component real vectors, realized as maps $Fin n to R$. The upstream definition states that $tPulledConnection$ equals $-(x i)^{-1}$ precisely when $i = j = k$ and equals zero otherwise; its documentation describes it as 'The flat t-connection pulled back through t_i = log x_i.' This supplies the diagonal Christoffel term $Gamma^i_{ii} = -1/x_i$ and sets up the projective-equivalence dichotomy between the one-dimensional and higher-dimensional cases.
proof idea
The proof is a one-line wrapper that applies the definition of tPulledConnection and simplifies using the hypothesis that the indices are not all equal.
why it matters
The result supplies the off-diagonal vanishing needed to complete the explicit form of the pulled connection. It supports the module's demonstration that the one-dimensional case is projectively equivalent to the zero connection while the case $n geq 2$ is not, as stated in the module documentation. No downstream citations are recorded, yet the lemma underpins the projective-equivalence dichotomy for dimensions greater than one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.