ProjectivelyEquivalentToZeroAt
ProjectivelyEquivalentToZeroAt defines when an n-dimensional affine connection Γ satisfies projective equivalence to zero via an auxiliary vector ψ. Researchers examining pulled-back flat connections in logarithmic coordinates cite it to separate the one-dimensional case from higher dimensions. The declaration is a direct existential definition that encodes the componentwise relation using the Kronecker delta.
claimAn affine connection Γ : Fin n → Fin n → Fin n → ℝ is projectively equivalent to zero if there exists a vector ψ : Fin n → ℝ such that Γ_{i j k} = δ_{i j} ψ_k + δ_{i k} ψ_j for all i, j, k ∈ Fin n.
background
The module records coefficient formulas for affine connections in x- and t-coordinates, where t = log x produces affine-flat connections that acquire the diagonal Christoffel term Γ^i_{ii} = −1/x_i upon pullback. Vec n is the type of n-component real vectors (Fin n → ℝ). The Kronecker delta delta(i, j) equals 1 when i = j and 0 otherwise, supplying the standard symbol used to build the projective condition.
proof idea
This is a direct definition. The body introduces an existential quantifier over a vector ψ of type Vec n and asserts the componentwise equality Γ i j k = delta i j * ψ k + delta i k * ψ j for all indices.
why it matters in Recognition Science
The definition supplies the predicate used by projectivelyEquivalent_one_dim (which proves equivalence holds for n = 1 on the t-pulled connection) and not_projectivelyEquivalentToZeroAt_tPulledConnection (which shows failure for n ≥ 2). It thereby realizes the module's stated dichotomy between one and higher dimensions for connections arising in the cost model. The construction is consistent with the affine-flat structure in logarithmic coordinates that the Recognition framework employs for N-dimensional extensions.
scope and limits
- Does not verify the property for any concrete connection such as tPulledConnection.
- Does not impose bounds on n or additional regularity conditions on Γ.
- Does not relate the condition to curvature, torsion, or the J-cost function.
- Does not address existence or uniqueness of ψ beyond the existential statement.
formal statement (Lean)
31def ProjectivelyEquivalentToZeroAt {n : ℕ}
32 (Γ : Fin n → Fin n → Fin n → ℝ) : Prop :=
proof body
Definition body.
33 ∃ ψ : Vec n, ∀ i j k : Fin n,
34 Γ i j k = delta i j * ψ k + delta i k * ψ j
35