loop_holonomy
plain-language theorem explainer
The definition computes the net rotation angle around a closed path of hinges by summing the individual deficit angles from each rotation in the list. Researchers deriving conservation laws in discrete gravity models cite this when applying the discrete Bianchi identity. It is implemented as a direct summation after mapping each hinge rotation to its angle.
Claim. For a finite list of hinge rotations each carrying a deficit angle $θ_i$, the net holonomy angle is $∑_i θ_i$.
background
The DiscreteBianchi module develops the discrete version of the Bianchi identity in Regge calculus on a lattice, where curvature appears as deficit angles at hinges. A hinge rotation is an element of SO(3) specified by an axis in three dimensions and the magnitude of the rotation angle, which equals the deficit. The module states that this identity constrains deficit angles at neighbouring hinges and, combined with the Regge equations, forces discrete energy-momentum conservation.
proof idea
The definition is a one-line wrapper that applies the sum operation to the list of angles obtained by mapping each hinge rotation to its angle field.
why it matters
This definition underpins the discrete_bianchi_identity in the same module, which states that the sum of signed deficit angles around a vertex vanishes modulo 2π. In the Recognition Science framework it realizes the geometric constraint analogous to the continuum Bianchi identity, thereby ensuring conservation laws follow from the Einstein-like equations on the lattice. It aligns with the forcing of three spatial dimensions through the structure of rotations in the perpendicular planes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.