Registry · Definition II.D80 tau-effective formalized

II.D80 — τ-Curvature

Curvature R(v,w)(x) = Γ(Γ(x,v),w) - Γ(Γ(x,w),v) measures parallel transport non-commutativity. For the flat connection on Z/M_k Z, R = 0.

Book II Part 10 Ch. 55

Dependency Graph

Depends on (2)

II.D78 II.D79

Depended on by (1)

II.T51

Lean Formalization

Module: TauLib.BookII.Closure.Curvature

Symbol: curvature_check