linearized_implies_general
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the Bianchi identity from first principles without the linearized hypothesis.
- Does not extend to nonlinear or large-deficit regimes.
- Does not address the continuum limit or higher-dimensional lattices.
formal statement (Lean)
87theorem linearized_implies_general (deficits : List ℝ)
88 (h : linearized_bianchi deficits) :
89 discrete_bianchi_identity deficits :=
proof body
Term-mode proof.
90 ⟨0, by unfold linearized_bianchi at h; simp [h]⟩
91
92/-- For a flat lattice, all deficits are zero, so Bianchi is trivially satisfied. -/