pith. machine review for the scientific record. sign in
def definition def or abbrev

loop_holonomy

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  56def loop_holonomy (rotations : List HingeRotation) : ℝ :=

proof body

Definition body.

  57  (rotations.map HingeRotation.angle).sum
  58
  59/-! ## The Discrete Bianchi Identity -/
  60
  61/-- **DISCRETE BIANCHI IDENTITY (Hamber-Kagel)**:
  62    The product of rotation matrices along any null-homotopic path
  63    through the dual lattice is the identity matrix.
  64
  65    In terms of deficit angles: for any closed loop of hinges sharing
  66    a common vertex, the sum of (signed) deficit angles equals zero
  67    modulo 2*pi.
  68
  69    More precisely: for the hinges h_1, ..., h_n forming a closed
  70    path around a vertex v in the dual complex:
  71      sum_{i=1}^n delta_{h_i} = 0  (mod 2*pi)
  72
  73    In the linearized (small-angle) regime, this becomes:
  74      sum_{i=1}^n delta_{h_i} = 0  (exactly)
  75
  76    This is the geometric identity that, combined with the Regge
  77    equations, forces discrete energy-momentum conservation. -/

depends on (19)

Lean names referenced from this declaration's body.