Cost Ndim Connections Projectively Equivalent One Dim

The one-dimensional exception

An affine connection is a rule for comparing directions at nearby points, the mathematical skeleton beneath the idea of parallel transport. In coordinates where the comparison looks flat, the connection's coefficients vanish. Change coordinates and those coefficients reappear, encoding the curvature of the coordinate map itself rather than any intrinsic geometry. The Recognition Science framework's library records a precise fact about this bookkeeping: in one dimension, any such connection can be made to look flat by a projective transformation, while in two or more dimensions that freedom disappears.

The framework works with two coordinate systems. The first, called x-coordinates, is the direct description of a point by its components. The second, t-coordinates, applies the map t = log x to each component, a standard change that turns multiplicative scaling into additive translation. In t-coordinates the connection is flat by construction: its coefficients are all zero. Pulling that flat connection back through the logarithm into x-coordinates produces a diagonal term, the only surviving coefficient being -1/x for each component.

The theorem projectivelyEquivalent_one_dim proves that for a single component, this pulled-back connection is projectively equivalent to the zero connection. Projective equivalence here means there exists a vector field ψ such that the connection coefficients take the form Γⁱ_jk = δ^{i_jψ_k + δi_kψ_j. For one dimension, the witness is simply ψ = -1/(2x), and the proof checks the identity by cases on the single index. The companion theorem shows the contrast: for any dimension n ≥ 2, with all components nonzero, the pulled-back connection is not projectively equivalent to the zero connection.}

What this establishes in plain terms is a dimension dichotomy. In one dimension, the logarithmic coordinate change can be undone by a projective adjustment, so the connection carries no residual obstruction. In higher dimensions, that adjustment fails: the diagonal terms from the logarithm cannot be absorbed by any single vector field, leaving a genuine projective invariant. The framework reads this as a structural reason why one dimension is special in its cost geometry, a fact that does not by itself say anything about physical space.

The declaration does not claim that one dimension is the only case with any projective flexibility, nor that the failure in higher dimensions implies anything about the number of spatial dimensions we inhabit. It proves a statement about connections and coordinate changes, nothing more. The physical interpretation, if any, belongs to later steps in the framework's chain, not to this theorem.

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

@[simp] theorem xFlatConnection_apply {n : ℕ} (x : Vec n) (i j k : Fin n) :
    xFlatConnection x i j k = 0 := rfl

What this page does not claim

The theorem does not claim that one dimension is the only case with any projective flexibility. It does not claim that the failure in higher dimensions implies anything about the number of spatial dimensions we inhabit. It does not claim any physical interpretation of the connection beyond the coordinate bookkeeping itself.

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: