Cost Ndim Connections Not Projectively Equivalent To Zero At T Pulled Connection

Why flatness fails in higher dimensions

An affine connection is a rule for comparing vectors at nearby points, the mathematical skeleton beneath the familiar idea of parallel transport. A connection is called flat when parallel transport around any small loop returns a vector unchanged, the same property that makes ordinary Euclidean space feel straight. In the framework's recognition cost analysis, a change of coordinates from x to t = log x is built to be flat by construction, a deliberate choice that makes the t-coordinates the natural reference frame.

When that flat t-connection is pulled back into the original x-coordinates, the formulas change. In one dimension, the pulled connection takes the form Γ¹₁₁ = -1/x, a single diagonal term that records how the logarithm warps the line. The framework's library proves that in one dimension this connection is projectively equivalent to the zero connection: there exists a function ψ such that Γ¹₁₁ = 2ψ, meaning the connection can be absorbed into a pure scaling effect. This is the theorem projectivelyEquivalent_one_dim, and it says that in one dimension the curvature can be completely disguised.

The declaration not_projectivelyEquivalentToZeroAt_tPulledConnection establishes the opposite for every dimension n ≥ 2. Its statement is precise: for any n with 2 ≤ n, any nonzero vector x, the pulled connection cannot be written in the form Γᵢⱼₖ = δᵢⱼψₖ + δᵢₖψⱼ for any choice of ψ. The diagonal term -1/xᵢ is forced to appear in a way that no single scaling function can absorb across multiple coordinates. The theorem is proved in the machine-checked library of formal theorems, with the proof resting on the structure of the Kronecker delta and the distinct diagonal entries.

What this means in plain language: in two or more dimensions, the logarithmic coordinate change leaves an irreducible trace in the connection coefficients. The flatness of the t-coordinates cannot be hidden by a projective re-scaling once the dimension exceeds one. This is not a statement about physics directly; it is a pure geometric fact about how flat connections behave under this specific coordinate pullback. The framework uses this dichotomy to mark a structural boundary between one-dimensional and multi-dimensional cost analysis, a boundary that the forcing chain later exploits when it derives three spatial dimensions.

The theorem does not claim that the pulled connection is curved, only that it is not projectively flat in the sense defined. It does not assert anything about the physical meaning of the coordinates, nor does it say that higher-dimensional recognition costs must be flat or curved. The result is a formal dichotomy: one dimension can disguise the connection, two or more cannot. That distinction is what makes the declaration a load-bearing step in the framework's dimensional argument.

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 theorem does not claim the pulled connection is curved or non-flat in the usual sense. It does not assert any physical interpretation of the coordinates or the connection coefficients. It does not claim that higher-dimensional recognition costs are projectively flat or that the dichotomy extends beyond the specific t = log x pullback.

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: