Cost Ndim Connections T Pulled Connection Off Diag

The off-diagonal flatness

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 a small loop returns a vector unchanged. A standard way to build a flat connection is to work in coordinates where the connection coefficients are identically zero, then pull the connection back to another coordinate system. The declaration tPulledConnection_offDiag records a fact about one such pullback in the Recognition Science framework's library: when the new coordinate is the logarithm of the old one, the pulled-back connection has nonzero coefficients only on the diagonal, and every off-diagonal coefficient is exactly zero.

The setup is concrete. Start with coordinates x and define new coordinates t by t_i = log x_i. In t-coordinates the connection is flat by construction. Pulling it back to x-coordinates produces a connection whose diagonal coefficient at index i is -1/x_i, the familiar Christoffel term. The theorem tPulledConnection_offDiag states the complementary half: whenever the three indices are not all equal, the coefficient is 0. The proof is a direct unfolding of the definition, and the result holds for any dimension n and any vector x whose entries are nonzero.

The useful consequence is a clean dichotomy about projective equivalence, which asks whether two connections differ only by a vector field term. In one dimension, the pulled-back connection is projectively equivalent to the zero connection. In two or more dimensions, this fails: the framework's library proves that no such equivalence exists when n is at least 2 and all coordinates are nonzero. The off-diagonal theorem supplies the algebraic fact that makes the failure sharp: because the connection is purely diagonal, any projective equivalence would have to absorb the entire -1/x_i term into the vector field, which the dimension count forbids.

Within Recognition Science, this is a structural lemma about the geometry of the cost function's coordinates, not a claim about physics. The theorem does not say that space is flat, that the connection is the Levi-Civita connection of a metric, or that any particular physical force follows. It is a statement about a coordinate transformation and the resulting connection coefficients, and it is proved in the framework's machine-checked library of formal theorems.

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

This theorem does not claim that physical space is flat or that the connection is the Levi-Civita connection of a metric. It does not claim that the off-diagonal coefficients vanish for any coordinate change other than t_i = log x_i. It does not claim that the connection is projectively equivalent to zero in dimensions two or higher.

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: