tPulledConnection
plain-language theorem explainer
The definition supplies the Christoffel symbols of the flat connection in logarithmic t-coordinates after pullback to the original x-variables. Researchers analyzing the Recognition Science cost model in multiple dimensions cite it when verifying the projective equivalence dichotomy. It is realized by a direct conditional that returns the inverse term only on the triple diagonal and zero elsewhere.
Claim. For a vector $x : Fin n → ℝ$ and indices $i,j,k : Fin n$, the pulled-back connection coefficient equals $-(x_i)^{-1}$ when $i = j = k$ and equals zero otherwise.
background
In the Recognition Science cost model the change of coordinates $t_i = log x_i$ renders the connection affine-flat by construction. The module records the explicit pullback of this flat connection to the original x-coordinates, where the only nonzero Christoffel symbols are the diagonal terms $Γ^i_{ii} = -1/x_i$. This supplies the coefficient formulas needed for the subsequent projective-equivalence statements. Vec is the type of n-component real vectors realized as functions Fin n → ℝ; it is introduced in the Core module as the basic coordinate object for the logarithmic aggregate.
proof idea
The definition is realized directly by a conditional expression: it returns -(x i)^{-1} precisely on the triple diagonal i = j = k and returns zero in every other case. No lemmas or tactics are applied; the body is the explicit formula.
why it matters
This definition is invoked by the theorems projectivelyEquivalent_one_dim and not_projectivelyEquivalentToZeroAt_tPulledConnection that establish the projective-equivalence dichotomy (one dimension versus n ≥ 2). It supplies the concrete coefficients required to verify those statements inside the affine-connection module. Within the Recognition framework it supports the geometric analysis of the cost functional in higher dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.