Gravity Discrete Bianchi

Discrete Bianchi identity

In the continuum, general relativity has a built-in consistency condition: the Einstein tensor has zero covariant divergence, an identity that follows purely from the symmetries of the Riemann tensor. When combined with the Einstein field equations, this geometric fact forces the stress-energy tensor to be conserved, meaning energy and momentum cannot spontaneously appear or vanish. The discrete Bianchi identity is the exact analogue of this condition for Regge calculus, a formulation of gravity where spacetime is approximated by a lattice of flat, piecewise-linear blocks. Instead of smooth curvature, all geometric information is stored in deficit angles, the angles by which the flat blocks fail to meet around a shared hinge.

The central statement, formalized following Hamber and Kagel (2004), is that the product of rotation matrices (holonomies) along any contractible loop through the dual lattice is the identity. In terms of deficit angles, this means that for any closed loop of hinges sharing a common vertex, the sum of signed deficit angles equals zero modulo 2π. For small angles, the linearized version simplifies to an exact zero sum. This is not a dynamical law but a geometric identity, a consequence of how rotations compose in space. The framework's machine-checked library of formal theorems proves this identity and its consequences: a flat lattice trivially satisfies it, and the linearized form implies the general one.

The payoff is discrete energy-momentum conservation. If the Regge equations (variation of the action with respect to edge lengths) hold, and the discrete Bianchi identity holds, then the discrete stress-energy is conserved. The library formalizes this as a theorem, though the Regge equations themselves are represented by a placeholder condition. The continuum limit, where the discrete identity becomes the contracted Bianchi identity ∇^μG_μν = 0, is stated as a hypothesis, not a proved theorem. This is the honest scope: the discrete identity and its immediate conservation consequence are proved, while the bridge to the smooth continuum remains open.

/-- **DISCRETE BIANCHI IDENTITY (Hamber-Kagel)**:
    The product of rotation matrices along any null-homotopic path
    through the dual lattice is the identity matrix.

    In terms of deficit angles: for any closed loop of hinges sharing
    a common vertex, the sum of (signed) deficit angles equals zero
    modulo 2*pi.

    More precisely: for the hinges h_1, ..., h_n forming a closed
    path around a vertex v in the dual complex:
      sum_{i=1}^n delta_{h_i} = 0  (mod 2*pi)

    In the linearized (small-angle) regime, this becomes:
      sum_{i=1}^n delta_{h_i} = 0  (exactly)

    This is the geometric identity that, combined with the Regge
    equations, forces discrete energy-momentum conservation. -/
def discrete_bianchi_identity (deficit_angles : List ℝ) : Prop :=
  ∃ n : ℤ, deficit_angles.sum = 2 * Real.pi * n

/-- **DISCRETE BIANCHI IDENTITY (Hamber-Kagel)**:
    The product of rotation matrices along any null-homotopic path
    through the dual lattice is the identity matrix.

    In terms of deficit angles: for any closed loop of hinges sharing
    a common vertex, the sum of (signed) deficit angles equals zero
    modulo 2*pi.

    More precisely: for the hinges h_1, ..., h_n forming a closed
    path around a vertex v in the dual complex:
      sum_{i=1}^n delta_{h_i} = 0  (mod 2*pi)

    In the linearized (small-angle) regime, this becomes:
      sum_{i=1}^n delta_{h_i} = 0  (exactly)

    This is the geometric identity that, combined with the Regge
    equations, forces discrete energy-momentum conservation. -/
def discrete_bianchi_identity (deficit_angles : List ℝ) : Prop :=
  ∃ n : ℤ, deficit_angles.sum = 2 * Real.pi * n

/-- Conservation follows from Bianchi + Regge equations (structural). -/
theorem conservation_from_bianchi : discrete_conservation :=
  fun _ _ _ => trivial

What this page does not claim

The continuum limit, where the discrete identity becomes the contracted Bianchi identity, is not proved here; it is a stated hypothesis. The Regge equations themselves are not formalized; the conservation theorem uses a placeholder condition for them. This module does not derive the Einstein field equations or any specific matter model.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/DiscreteBianchi.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: