Cost Ndim Connections Delta

The delta symbol

The Kronecker delta is a function of two indices that returns 1 when they are equal and 0 otherwise. Written as δᵢⱼ, it is one of the most common bookkeeping devices in mathematics, used to compress sums and to define identity matrices. In the Recognition Science framework, this same symbol appears in a geometric role: it records which coefficients of a connection survive when coordinates are changed.

The framework works with a cost function J(x) = (x + 1/x)/2 - 1, which is proved to be the unique function satisfying five plain conditions. A standard change of variables t = log x makes the geometry flat by construction, meaning its connection coefficients are all zero. When that flat geometry is pulled back to the original x-coordinates, the connection gains a diagonal term: Γⁱᵢᵢ = -1/xᵢ. This is where the delta appears, selecting exactly the diagonal entries of the connection.

The delta also marks a sharp dimensional divide. In one dimension, the pulled-back connection is projectively equivalent to the zero connection, meaning a suitable reparametrization can remove its curvature entirely. In two or more dimensions, this fails: no such reparametrization exists. The framework's library proves both facts as theorems, with the one-dimensional case holding and the higher-dimensional case failing for any dimension n ≥ 2.

In Recognition Science, this dichotomy matters because the framework derives three spatial dimensions from its forcing chain. The delta's behavior is a local geometric fact that supports that derivation, but it is not itself the derivation. The delta does not define the cost function, does not force the number of dimensions, and does not establish any physical law. It is a precise mathematical tool, and its role is to mark where the geometry changes character.

/-- The Kronecker delta on `Fin n`. -/
def delta {n : ℕ} (i j : Fin n) : ℝ :=
  if i = j then 1 else 0

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

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 delta does not define the cost function J. The delta does not by itself force the number of spatial dimensions. The projective equivalence theorem does not assert any physical law about actual space.

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: