projectivelyEquivalent_one_dim
plain-language theorem explainer
In one dimension the connection obtained by pulling back the flat t-connection via t = log x is projectively equivalent to the zero connection. Researchers analyzing affine structures within the Recognition Science cost framework cite this result for the one-dimensional reduction. The proof supplies an explicit vector field ψ equal to minus half the reciprocal of the single coordinate and verifies the defining relation by exhaustive case analysis on the single index triple.
Claim. Let $x$ be a one-dimensional vector and let $Γ$ be the connection with coefficients $Γ_{ijk} = -(x_i)^{-1}$ when $i=j=k$ and zero otherwise. Then there exists a vector $ψ$ such that $Γ_{ijk} = δ_{ij} ψ_k + δ_{ik} ψ_j$ for all indices $i,j,k$.
background
The module records affine connections in $x$- and $t$-coordinates with $t_i = log x_i$. The $t$-coordinates are affine-flat by construction; the pullback to $x$-coordinates produces the diagonal term $Γ^i_{ii} = -1/x_i$ and establishes the projective equivalence dichotomy between dimension one and higher dimensions. ProjectivelyEquivalentToZeroAt($Γ$) asserts existence of a vector $ψ$ such that $Γ i j k = δ_{ij} ψ_k + δ_{ik} ψ_j$ for all indices, where $δ$ is the Kronecker delta. tPulledConnection($x$) returns $-(x_i)^{-1}$ precisely on the triple where $i=j=k$ and zero elsewhere. Vec $n$ is the type of maps from Fin $n$ to the reals.
proof idea
The term-mode proof constructs the witness $ψ$ as the constant map sending the single index to $-(x_0)^{-1}/2$. It then introduces the indices $i,j,k$, applies fin_cases three times to reduce to the sole triple $(0,0,0)$, and invokes simp on delta and tPulledConnection to confirm both sides of the required equality agree.
why it matters
This theorem supplies the one-dimensional half of the projective equivalence dichotomy stated in the module documentation. The module records that the one-dimensional case is projectively equivalent to the zero connection while the property fails for $n ≥ 2$. It thereby closes the base case for the analysis of pulled-back affine connections arising from the logarithmic coordinate change in the cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.