HingeRotation
plain-language theorem explainer
HingeRotation encodes a single rotation about one of three axes by a real angle, serving as the elementary holonomy element in discrete Regge calculus. Workers on lattice gravity and discrete Bianchi identities cite it when building loop products that enforce curvature constraints. The declaration is a bare structure with no computational reduction or lemmas.
Claim. A hinge rotation is a pair consisting of an axis index $a$ in the finite set of three coordinate directions together with a real angle $θ$, representing the rotation in the plane perpendicular to that axis whose magnitude equals the curvature deficit at the hinge.
background
The DiscreteBianchi module formalizes the exact discrete Bianchi identity for Regge calculus after Hamber and Kagel, the lattice counterpart of the contracted identity that forces energy-momentum conservation once the Einstein equations hold. In three dimensions the hinge is an edge and the associated rotation lies in the two-plane normal to it. Upstream dependencies supply auxiliary structures for J-cost convexity, spectral emergence of gauge groups, and spin assignments, but the local setting is fixed by the ReggeCalculus import that supplies the underlying simplicial geometry.
proof idea
Direct structure definition introducing two fields: axis of type Fin 3 and angle of type real. No tactics or lemmas are invoked; the declaration simply packages the data type for subsequent use in composition and summation operations.
why it matters
The structure supplies the input type for compose_same_axis, which adds angles on a shared axis, and for loop_holonomy, which sums angles around closed paths. These constructions realize the discrete Bianchi identity whose contractible-loop product equals the identity, thereby deriving the discrete conservation law. It anchors the Regge-calculus sector of the Recognition framework at the D = 3 level fixed by the eight-tick octave and supplies the geometric carrier for deficit-angle constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.