compose_same_axis
plain-language theorem explainer
This definition combines two hinge rotations sharing an axis by adding their angles while keeping the axis fixed. It is used in constructions of discrete holonomies for Regge calculus models of gravity. The implementation is a direct structure constructor that sums the angles under the shared-axis hypothesis.
Claim. For hinge rotations $r_1$ and $r_2$ with identical axis, the composition is the hinge rotation whose axis equals that common value and whose angle equals the sum of the two angles.
background
HingeRotation is a structure with an axis in Fin 3 and a real angle, representing a rotation in the plane perpendicular to a hinge; in 3D the hinge is an edge and the angle equals the deficit angle. The module formalizes the discrete Bianchi identity for Regge calculus following Hamber and Kagel, the discrete analog of the contracted Bianchi identity that enforces energy-momentum conservation when combined with the Einstein equations. This definition supplies the basic operation for composing rotations along paths of hinges.
proof idea
The definition is a one-line wrapper that constructs a new HingeRotation by taking the shared axis and adding the angles from the two inputs.
why it matters
This definition supports the construction of holonomy products around loops, which is the key step toward the discrete Bianchi identity and the derived conservation laws in the module. It aligns with the Hamber-Kagel approach to discrete gravity and the Recognition Science treatment of geometric identities at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.