Cost Ndim Connections Projectively Equivalent To Zero At

Projective equivalence

In differential geometry, two affine connections are projectively equivalent when they have the same geodesics up to reparametrization: a curve that is a straight line under one connection is also a straight line under the other, though it may be traversed at a different speed. The zero connection, whose Christoffel symbols all vanish, describes the usual flat geometry of Euclidean space. A connection is projectively equivalent to zero when there exists a vector field ψ such that its Christoffel symbols take the form Γⁱ_{jk} = δⁱ_j ψ_k + δⁱ_k ψ_j. This is a standard and classical condition, not an invention of the framework.

The framework's recognition cost, the forced price of maintaining a ledger of recognition events, is defined in coordinates where x is the variable of interest. Its natural flat connection in the logarithmic coordinate t = log x pulls back to a connection in x-coordinates with diagonal Christoffel symbols Γⁱ_{ii} = −1/xᵢ and all off-diagonal terms zero. The declaration ProjectivelyEquivalentToZeroAt asks whether this pulled-back connection is projectively equivalent to the zero connection. The framework's library proves the dichotomy: in one dimension it is, and in two or more dimensions it is not, provided no coordinate is zero.

The one-dimensional proof is constructive. The library exhibits the explicit ψ vector, namely ψ = −1/(2x), and verifies the identity by direct computation. In higher dimensions, the proof shows that no such ψ can exist. The geometric meaning is that in one dimension every connection is projectively flat, because there is only one direction for a geodesic to go; in two or more dimensions, the diagonal singularity −1/xᵢ cannot be absorbed by a projective reparametrization. This is a precise, machine-checked statement about the framework's coordinate geometry, not a claim about physical space.

The declaration does not claim that the framework's cost function is projectively flat in physical space, nor that the pulled-back connection is the unique connection with this property. It only records a technical fact about the coordinate transformation used in the framework's derivations. The result is a lemma in the framework's internal geometry, useful for understanding why the one-dimensional cost equation behaves differently from its higher-dimensional analogues.

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 declaration does not claim that the framework's cost function is projectively flat in physical space. The declaration does not claim that the pulled-back connection is the unique connection with the stated property. The declaration does not claim any physical consequence about the dimensionality of 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: