ProjectivelyEquivalentToZeroAt
plain-language theorem explainer
ProjectivelyEquivalentToZeroAt defines when an affine connection Γ on n dimensions satisfies projective equivalence to the zero connection, namely when there exists a vector ψ such that Γ i j k equals delta i j times ψ k plus delta i k times ψ j. Researchers analyzing affine structures in the cost domain cite this predicate to separate the one-dimensional case from higher dimensions. The definition is a direct existential statement over ψ with no auxiliary lemmas.
Claim. A connection Γ is projectively equivalent to the zero connection when there exists a vector ψ such that for all indices i, j, k one has Γ_{ijk} = δ_{ij} ψ_k + δ_{ik} ψ_j.
background
Vec n is the type of n-component real vectors, written as maps from Fin n to ℝ. The function delta is the Kronecker delta: delta i j equals 1 when i = j and 0 otherwise. The module records how the flat connection in t = log x coordinates pulls back to x-coordinates, acquiring the diagonal term Γ^i_{ii} = −1/x_i. This definition isolates the precise algebraic condition under which the pulled-back connection remains projectively equivalent to the zero connection.
proof idea
The declaration is a definition whose body is the direct existential quantification ∃ ψ : Vec n, ∀ i j k, Γ i j k = delta i j * ψ k + delta i k * ψ j. No lemmas are invoked; the statement simply encodes the projective correction term using the Kronecker delta supplied by the upstream delta definition.
why it matters
The definition supplies the predicate used by projectivelyEquivalent_one_dim, which shows the condition holds for the one-dimensional t-pulled connection, and by not_projectivelyEquivalentToZeroAt_tPulledConnection, which shows it fails for n ≥ 2. It therefore realizes the projective-equivalence dichotomy stated in the module documentation. Within Recognition Science this supports the treatment of affine connections that arise when the forcing chain reaches D = 3 and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.