linearized_implies_general
plain-language theorem explainer
The theorem shows that any list of real deficit angles satisfying the linearized Bianchi identity must satisfy the full discrete Bianchi identity. Workers in Regge calculus and discrete gravity models would cite this reduction when moving from linear approximations to exact constraints. The proof is a direct term construction that unfolds the linearized hypothesis and simplifies to witness the general identity.
Claim. Let $d$ be a list of real numbers representing deficit angles. If $d$ satisfies the linearized Bianchi identity, then $d$ satisfies the discrete Bianchi identity.
background
The DiscreteBianchi module formalizes the exact discrete Bianchi identity for Regge calculus following Hamber and Kagel (2004). This is the discrete analog of the contracted Bianchi identity nabla^mu G_mu_nu = 0 from continuum GR, which forces energy-momentum conservation when paired with the Einstein equations. In the discrete setting the identity constrains deficit angles at neighbouring hinges by requiring the product of holonomy rotation matrices around any contractible loop to equal the identity.
proof idea
This is a term-mode proof that constructs the required witness for the general identity. It unfolds the linearized_bianchi hypothesis at the supplied assumption and applies simp to discharge the discrete_bianchi_identity goal, returning a structure containing zero together with the simplified proof term.
why it matters
The result is invoked inside discrete_bianchi_cert to certify that the linearized case implies the general identity, alongside the flat case and the conservation law derived from Bianchi. It fills the discrete analog of the Bianchi identity step in the Recognition framework, supporting the derivation of conservation laws from geometric identities and aligning with the forcing chain landmarks that produce D = 3 and the eight-tick octave. The proof is complete with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.