not_projectivelyEquivalentToZeroAt_tPulledConnection
plain-language theorem explainer
For n at least 2 and vectors x in R^n with every component nonzero, the pulled-back connection with diagonal term -1/x_i fails to be projectively equivalent to the zero connection. Researchers on affine structures within Recognition Science cite the result to enforce the dimensional split between the one-dimensional case and higher dimensions. The proof assumes an equivalence via some auxiliary vector ψ, evaluates the relation on a pair of distinct indices to force a component of ψ to zero, and reaches a contradiction with the inverse of a non-
Claim. Let $n$ be a natural number with $n$ at least 2. Let $x$ be a map from the set of indices $0$ to $n-1$ into the reals such that every value $x_i$ is nonzero. Define the connection coefficients by setting them equal to $-x_i^{-1}$ precisely when the three indices coincide and zero otherwise. Then no vector field ψ exists satisfying the identity that the connection equals the sum of the Kronecker delta times ψ on the last index plus the Kronecker delta times ψ on the middle index, for every triple of indices.
background
The module records affine connections in x- and t-coordinates. The change of coordinate t_i = log x_i renders the connection affine-flat; its pull-back to x-coordinates produces the diagonal term Γ^i_{ii} = -1/x_i. The module proves the projective-equivalence dichotomy: the one-dimensional case is equivalent to the zero connection while dimensions n ≥ 2 are not. ProjectivelyEquivalentToZeroAt Γ asserts the existence of a vector ψ such that Γ_{i j k} equals delta_{i j} ψ_k plus delta_{i k} ψ_j for all indices, where delta is the Kronecker symbol that returns 1 on equal arguments and 0 otherwise. tPulledConnection x returns -x_i^{-1} exactly on the triple (i,i,i) and zero elsewhere. Vec n denotes the type of real-valued functions on the finite set of n indices.
proof idea
The tactic proof first constructs two distinct indices i0 = 0 and i1 = 1, which exist because n ≥ 2. It assumes for contradiction that some ψ realizes projective equivalence. Substituting the triple (i0, i0, i1) into the equivalence forces ψ at i1 to vanish, since the left-hand side is zero. The same equivalence applied to the triple (i1, i1, i1) then equates -x_{i1}^{-1} to twice the zero value of ψ at i1, implying that the inverse vanishes and contradicting the hypothesis that x at i1 is nonzero.
why it matters
The declaration completes the projective-equivalence dichotomy recorded in the module documentation for the cost geometry. It isolates the failure of projective triviality for the t-pulled connection precisely when the dimension reaches two or more, aligning with the framework requirement of three spatial dimensions. No downstream theorems are recorded, so the result functions as a basic lemma supporting later arguments that distinguish the one-dimensional reduction from the full n-dimensional cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.