DiscreteBianchiCert
plain-language theorem explainer
DiscreteBianchiCert packages three properties that connect vanishing deficit angles to the linearized Bianchi identity, the linearized case to the full discrete Bianchi identity, and a discrete conservation law. Regge-calculus modelers cite it when certifying the passage from discrete holonomy constraints to continuum conservation. The structure is assembled by direct field assignment from the sibling lemmas flat_bianchi, linearized_implies_general, and conservation_from_bianchi.
Claim. A structure asserting that, for any list of deficit angles, (i) all angles zero implies their sum is zero, (ii) sum zero implies the sum equals $2π n$ for some integer $n$, and (iii) the discrete conservation law holds whenever the Regge equations and linearized Bianchi identity are satisfied.
background
The module formalizes the discrete Bianchi identity in Regge calculus following Hamber and Kagel. The upstream definition discrete_bianchi_identity states that the product of rotation matrices along any null-homotopic path through the dual lattice is the identity, equivalently that the sum of signed deficit angles around a closed loop equals $2π n$ for integer $n$. linearized_bianchi is the small-angle reduction requiring the sum to be exactly zero. discrete_conservation encodes that the Regge equations together with the Bianchi identity force discrete stress-energy conservation, mirroring the continuum relation between the contracted Bianchi identity and energy-momentum conservation.
proof idea
Structure definition that directly bundles the three fields flat_ok, linearized_implies, and conservation. Each field is supplied by a sibling definition: flat_ok from flat_bianchi, linearized_implies from linearized_implies_general, and conservation from conservation_from_bianchi.
why it matters
The certificate is instantiated by the downstream theorem discrete_bianchi_cert and supplies the discrete-to-continuum bridge for the contracted Bianchi identity nabla^mu G_mu_nu = 0. In the Recognition framework it closes the step from discrete holonomy constraints to conservation, consistent with the geometric origin of the Bianchi identity in the eight-tick octave and three-dimensional spatial structure. It leaves open the rigorous derivation of the full continuum limit from the discrete Regge action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.