loop_holonomy

formal source

  53  ⟨r1.axis, r1.angle + r2.angle⟩
  54
  55/-- A path of rotations around a loop of hinges. -/
  56def loop_holonomy (rotations : List HingeRotation) : ℝ :=
  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. -/
  78def discrete_bianchi_identity (deficit_angles : List ℝ) : Prop :=
  79  ∃ n : ℤ, deficit_angles.sum = 2 * Real.pi * n
  80
  81/-- In the linearized regime (small deficit angles), the Bianchi
  82    identity reduces to: sum of deficit angles = 0 exactly. -/
  83def linearized_bianchi (deficit_angles : List ℝ) : Prop :=
  84  deficit_angles.sum = 0
  85
  86/-- The linearized Bianchi identity implies the general one (with n = 0). -/