discrete_bianchi_cert
plain-language theorem explainer
The discrete_bianchi_cert theorem constructs a certificate verifying the discrete Bianchi identity in Regge calculus by supplying the flat-lattice case, the implication from linearized to general identities, and the derived conservation law. Researchers modeling discrete gravity via Regge calculus would reference it to establish that the geometric constraint implies energy-momentum conservation. The proof proceeds as a direct structure instantiation referencing three supporting lemmas.
Claim. The structure DiscreteBianchiCert holds, where: for any list of deficits, if all are zero then the linearized Bianchi identity is satisfied; if the linearized Bianchi identity holds then the discrete Bianchi identity holds; and the discrete conservation law is satisfied.
background
In the DiscreteBianchi module, the discrete Bianchi identity is formalized as the exact analog in Regge calculus of the contracted Bianchi identity nabla^mu G_mu_nu = 0 from continuum general relativity, following Hamber and Kagel (2004). The key definitions include linearized_bianchi, which is the first-order version for small deficits, discrete_bianchi_identity as the general constraint on deficit angles, and discrete_conservation as the resulting conservation law. Upstream results establish that the flat case (all deficits zero) satisfies the linearized identity, that the linearized version implies the general one, and that conservation follows structurally from the Bianchi identity.
proof idea
The proof is a term-mode construction of the DiscreteBianchiCert structure. It directly assigns the flat_ok field to the flat_bianchi theorem, the linearized_implies field to the linearized_implies_general theorem, and the conservation field to the conservation_from_bianchi theorem.
why it matters
This declaration certifies the core discrete Bianchi identity for Regge calculus, which underpins the geometric origin of conservation laws in discrete gravity models. It directly supports the module's goal of showing that the discrete analog implies conservation, mirroring the continuum case where the Bianchi identity forces energy-momentum conservation. In the Recognition Science framework, it aligns with the forcing chain by providing a discrete geometric constraint consistent with the phi-ladder and self-similar structures, though the full continuum limit steps remain partially informal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.