H_bianchi_continuum_limit
plain-language theorem explainer
Researchers in discrete gravity and Regge calculus cite this definition to encode the continuum limit of the discrete Bianchi identity, where the linearized sum of deficit angles implies the contracted Bianchi identity nabla^mu G_mu_nu = 0. It sits in the DiscreteBianchi module as the target statement bridging Hamber-Kagel holonomy constraints to continuum conservation. The declaration is a direct one-line definition that wraps the implication from linearized_bianchi to the continuum claim without additional derivation.
Claim. The continuum hypothesis is the proposition that for every list of real numbers (deficit angles), if their sum equals zero (the linearized Bianchi identity), then the contracted Bianchi identity holds: $nabla^mu G_{mu nu} = 0$.
background
The DiscreteBianchi module formalizes the exact discrete Bianchi identity for Regge calculus following Hamber and Kagel (2004). It states that the product of rotation matrices (holonomies) along any null-homotopic path equals the identity, which constrains deficit angles at neighboring hinges and yields the discrete analog of nabla^mu G_mu_nu = 0. In continuum GR this identity is geometric and, paired with the Einstein equations, forces energy-momentum conservation.
proof idea
This is a one-line definition that directly encodes the forall implication to True. It applies the upstream linearized_bianchi definition (sum of deficit angles equals zero) from the same module and the mu projector from Cost.Ndim.Projector only indirectly via the broader gravity setup.
why it matters
The declaration supplies the hypothesis interface for the discrete-to-continuum transition in the Bianchi chain, linking to downstream results such as conservation_from_bianchi and discrete_conservation within the module. It fills the step from discrete holonomy around contractible loops to nabla^mu G_mu_nu = 0 as described in the module doc-comment, touching the open question of fully formalizing the Regge-to-Einstein limit in Recognition Science gravity models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.