linearized_bianchi
The linearized Bianchi identity requires that the sum of small deficit angles around any closed loop vanishes exactly. Discrete gravity researchers extending Regge calculus cite this reduction when deriving conservation laws in the weak-field limit. The statement is introduced directly by setting the property equal to the vanishing of the angle sum.
claimFor a list of small deficit angles $δ_i$, the linearized Bianchi identity holds precisely when $∑_i δ_i = 0$.
background
The module formalizes the discrete analog of the contracted Bianchi identity $∇^μ G_{μν} = 0$ in Regge calculus following Hamber and Kagel. Deficit angles measure curvature at hinges, and the full discrete version requires the product of holonomy matrices around contractible loops to equal the identity. The linearized form applies when angles remain small. Upstream results supply the basic one-elements from integer, rational, and spin constructions used to build the discrete structures.
proof idea
This is a definition that directly equates the property to the sum of the input list of real numbers equaling zero. No lemmas are applied.
why it matters in Recognition Science
It supplies the base case for DiscreteBianchiCert and enables linearized_implies_general together with discrete_conservation. The definition bridges discrete holonomy to the algebraic Bianchi identity, recovering $∇^μ G_{μν} = 0$ in the continuum limit and thereby enforcing energy-momentum conservation once the Einstein equations are imposed. It closes the step from discrete constraints to the recognition composition law in the gravity sector.
scope and limits
- Does not derive the full nonlinear discrete Bianchi identity from holonomy products.
- Does not specify how deficit angles are generated by the Regge action.
- Does not map the discrete identity to the Riemann tensor.
- Does not enforce the constraint for large angles.
formal statement (Lean)
83def linearized_bianchi (deficit_angles : List ℝ) : Prop :=
proof body
Definition body.
84 deficit_angles.sum = 0
85
86/-- The linearized Bianchi identity implies the general one (with n = 0). -/