discrete_bianchi_identity
plain-language theorem explainer
The discrete Bianchi identity is defined as the property that the sum of a list of deficit angles equals 2π times an integer. Workers deriving conservation laws from Regge calculus in the Recognition framework cite this when linking holonomy closure to energy-momentum balance. The definition directly encodes the condition that the product of rotation matrices around any contractible loop equals the identity.
Claim. For a list of real numbers $δ_1,…,δ_k$ representing deficit angles at hinges around a vertex, the discrete Bianchi identity holds when there exists an integer $n$ such that $∑_{i=1}^k δ_i = 2π n$.
background
In Regge calculus the deficit at a hinge is $2π$ minus the sum of the dihedral angles meeting there, as supplied by DihedralAngle.deficit. The module DiscreteBianchi formalizes the exact discrete analog of the contracted Bianchi identity $∇^μ G_{μν}=0$ from continuum GR, following Hamber and Kagel. Upstream results include the trivial holonomy product for contractible loops and the J-cost structures that calibrate the underlying geometry.
proof idea
This declaration is a definition. It states that the property holds precisely when the sum of the supplied deficit angles list equals 2π times some integer n.
why it matters
This definition supplies the core constraint used by DiscreteBianchiCert to certify passage from discrete holonomy to conservation. It fills the Hamber-Kagel step that, together with the Regge equations, forces discrete energy-momentum conservation. The downstream theorem linearized_implies_general shows that the linearized case (exact sum zero) implies the general form with n=0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.