tPulledConnection_diag
plain-language theorem explainer
Researchers in affine geometry and Recognition Science cite this result for the explicit diagonal Christoffel symbol arising from the pullback of the flat t-connection. It states that the coefficient at equal indices equals the negative reciprocal of the coordinate. The argument reduces directly via unfolding the piecewise definition.
Claim. For any natural number $n$, vector $x : Fin n → ℝ$, and index $i$, the pulled-back connection coefficient satisfies $Γ^i_{ii}(x) = -x_i^{-1}$.
background
The module records affine connections in x- and t-coordinates, where t = log x yields an affine-flat structure by construction. Pulling this connection back to x-coordinates produces the familiar diagonal term $Γ^i_{ii} = -1/x_i$ while off-diagonal entries vanish. Vec(n) is the type of n-component real vectors realized as functions Fin n → ℝ. The upstream definition tPulledConnection supplies the piecewise rule: the value is -(x i)^{-1} precisely when the three indices coincide and zero otherwise.
proof idea
The proof is a one-line wrapper that unfolds the definition of tPulledConnection and applies simplification to the conditional expression under the assumption i = j = k.
why it matters
This supplies the explicit diagonal coefficients required for the projective-equivalence dichotomy proved elsewhere in the module. It fills the coefficient formulas in the Recognition Science affine-connection setting, where the eight-tick octave and logarithmic coordinates enforce flatness in t-space and the standard -1/x_i term after pullback. The result supports downstream analysis of one-dimensional equivalence to the zero connection versus its failure for n ≥ 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.