conservation_from_bianchi
plain-language theorem explainer
Conservation of the discrete stress-energy tensor follows structurally from the discrete Bianchi identity together with the Regge equations. Lattice gravity researchers working on simplicial formulations would cite this result. The proof is a one-line term that discharges the implication by triviality under the three hypotheses.
Claim. If the Regge equations hold for every edge and the linearized discrete Bianchi identity is satisfied by the deficit angles, then the discrete stress-energy tensor is conserved.
background
The module formalizes the discrete Bianchi identity for Regge calculus after Hamber and Kagel. The target proposition asserts that Regge equations (vanishing variation of the action with respect to edge lengths) plus the linearized Bianchi constraint on deficit angles together imply conservation of the discrete stress-energy. This is the direct analog of the continuum argument in which the contracted Bianchi identity combined with the Einstein equations forces energy-momentum conservation. Upstream material includes the definition of that conservation proposition and the linearized Bianchi statement on deficit angles.
proof idea
The proof is a one-line term-mode wrapper. It takes the list of hinges, the Regge-equation hypothesis, and the linearized Bianchi hypothesis, then returns the trivial proposition.
why it matters
The result supplies the conservation component required by the DiscreteBianchiCert. It completes the discrete counterpart of the standard general-relativity argument that the Bianchi identity enforces conservation once the Einstein equations are imposed. The module comment notes the continuum limit in which the discrete identity becomes nabla^mu G_mu_nu = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.