Cost Ndim Connections T Pulled Connection Diag

The pulled connection

In differential geometry, an affine connection is a rule for comparing vectors at nearby points, and a connection is flat when parallel transport around any small loop brings a vector back unchanged. In the Recognition Science framework, the flat connection is first written in coordinates where each component is the logarithm of a positive number, t_i = log x_i. In those logarithmic coordinates the connection coefficients are all zero, which is the definition of affine-flat. The declaration tPulledConnection_diag records what happens when that same flat connection is pulled back to the original x-coordinates: on the diagonal, where all three indices are equal, the coefficient becomes the negative reciprocal of the coordinate, Γⁱ_ii = -1/x_i. Off the diagonal, all coefficients vanish. This is a theorem in the framework's machine-checked library of formal theorems, proved directly from the definition by simplification.

The interesting content is not the formula itself but what it means for projective equivalence. Two connections are projectively equivalent when they differ only by a term that preserves geodesics as unparametrized curves; the framework defines this precisely as the existence of a vector field ψ such that Γⁱ_jk = δ_ijψ_k + δ_ikψ_j. The framework proves a dichotomy. In one dimension, the pulled connection is projectively equivalent to the zero connection: the single diagonal term can be absorbed by a choice of ψ, so geodesics are unchanged. In two or more dimensions, this fails. The theorem not_projectivelyEquivalentToZeroAt_tPulledConnection shows that for any n ≥ 2, with all coordinates nonzero, the pulled connection is not projectively equivalent to the zero connection. The diagonal term cannot be removed by any projective transformation.

In Recognition Science, this result matters because the framework derives spatial structure from a cost function, and the logarithmic coordinates are the natural setting where that cost function becomes simple. The one-dimensional case is special: a single coordinate can be rescaled to hide the connection entirely. In higher dimensions, the geometry resists that simplification, and the diagonal term is an intrinsic feature of the pulled-back description. The theorem does not claim anything about the physical meaning of the connection, about whether the diagonal term corresponds to curvature (it does not; the connection is flat by construction), or about what happens when coordinates are zero. It is a statement about coordinate representations of a flat connection, proved for all positive coordinates.

theorem tPulledConnection_diag {n : ℕ} (x : Vec n) (i : Fin n) :
    tPulledConnection x i i i = -(x i)⁻¹ := by
  unfold tPulledConnection
  simp

theorem tPulledConnection_offDiag {n : ℕ} (x : Vec n) {i j k : Fin n}
    (hijk : ¬ (i = j ∧ j = k)) :
    tPulledConnection x i j k = 0 := by
  unfold tPulledConnection
  simp [hijk]

theorem projectivelyEquivalent_one_dim {x : Vec 1} :
    ProjectivelyEquivalentToZeroAt (tPulledConnection x) := by
  refine ⟨fun _ => -((x 0)⁻¹) / 2, ?_⟩
  intro i j k
  fin_cases i
  fin_cases j
  fin_cases k
  simp [delta, tPulledConnection]

theorem not_projectivelyEquivalentToZeroAt_tPulledConnection {n : ℕ}
    (hn : 2 ≤ n) (x : Vec n) (hx : ∀ i : Fin n, x i ≠ 0) :
    ¬ ProjectivelyEquivalentToZeroAt (tPulledConnection x) := by
  let i0 : Fin n := ⟨0, lt_of_lt_of_le (by decide : 0 < 2) hn⟩
  let i1 : Fin n := ⟨1, lt_of_lt_of_le (by decide : 1 < 2) hn⟩
  have hi01 : i0 ≠ i1 := by
    simp [i0, i1]
  intro hproj
  rcases hproj with ⟨ψ, hψ⟩
  have hpsi1 : ψ i1 = 0 := by
    have h := hψ i0 i0 i1
    simpa [eq_comm, delta, tPulledConnection, hi01] using h
  have hdiag : tPulledConnection x i1 i1 i1 = delta i1 i1 * ψ i1 + delta i1 i1 * ψ i1 := by
    simpa using hψ i1 i1 i1
  have hxinv_zero : (x i1)⁻¹ = 0 := by
    have h' : -(x i1)⁻¹ = 0 := by
      simpa [delta, tPulledConnection, hpsi1] using hdiag
    exact neg_eq_zero.mp h'
  exact (inv_ne_zero (hx i1)) hxinv_zero

What this page does not claim

The theorem does not claim the pulled connection has curvature; it is flat by construction. The theorem does not claim the diagonal term has physical meaning beyond its role in coordinate representations. The theorem does not cover coordinates that are zero or negative.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Ndim/Connections.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: