Cost Ndim Connections

Connections across dimensions

In differential geometry, an affine connection is a rule for comparing vectors at nearby points, and a flat connection is one where parallel transport around any small loop returns a vector unchanged. The module cost-ndim-connections studies a particular flat connection that arises when coordinates are transformed by logarithms. If the original coordinates are x and the new coordinates are t = log x, then the connection that is flat in t-coordinates becomes, in x-coordinates, a diagonal term Γⁱ_ii = −1/x_i. This is a standard change-of-coordinates calculation, and the module records the resulting coefficient formulas.

The interesting result is a dichotomy between dimensions. Two connections are projectively equivalent when they have the same geodesics up to reparametrization, which for this setting means the connection can be written as Γⁱ_jk = δ_ijψ_k + δ_ikψ_j for some vector ψ. The module proves that in one dimension, the pulled-back connection is projectively equivalent to the zero connection. In two or more dimensions, this fails: no such ψ exists, provided all coordinates x_i are nonzero. The one-dimensional case is special because a single coordinate leaves no room for the off-diagonal terms that obstruct the equivalence.

In Recognition Science, this distinction matters because the framework's cost function J(x) = (x + 1/x)/2 − 1 lives in one dimension, and the projective equivalence in that case is what lets the cost function inherit the flat geometry of log-coordinates. The failure in higher dimensions is a structural fact, not a computational inconvenience. It says that the simple geometric picture that works for the one-dimensional cost does not extend automatically to vector-valued costs, and any higher-dimensional generalization must confront this obstruction directly.

The module is a machine-checked library of formal theorems, and its two main results are proved with no unverified assumptions. The first, projectivelyEquivalent_one_dim, constructs the explicit ψ for the one-dimensional case. The second, not_projectivelyEquivalentToZeroAt_tPulledConnection, shows the negation for n ≥ 2. Together they give a precise boundary: one dimension is projectively flat, and every higher dimension is not.

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

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

What this page does not claim

This module does not prove that the cost function J is unique or that it arises from the connection geometry. The projective equivalence in one dimension does not imply the connection is flat in x-coordinates; it only shares geodesics with the zero connection. No claim is made about physical spacetime; the result is purely about the formal geometry of the coordinate change.

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: