Registry · Definition V.D43 tau-effective formalized

V.D43 — Holonomy gap element

The local gap element Delta_k^(n) = Phi_{k,k+1}^(n) - Id_{T^2} in End(T^2_{alpha_{k+1}}) measures the per-arc deviation from flatness. The total gap element at depth n sums these local contributions over all p_n arcs.

Book V Part 2 Ch. 11

Lean Formalization

Module: TauLib.BookV.GravityField.FrameHolonomy

Symbol: Tau.BookV.GravityField.HolonomyGapElement