Gravity Discrete Bianchi Conservation From Bianchi

The discrete conservation law

In general relativity, the Einstein field equations relate the curvature of spacetime to its matter content. A geometric identity, the contracted Bianchi identity, states that the divergence of the Einstein tensor is always zero. Combined with the field equations, this forces the divergence of the stress-energy tensor to vanish, which is the statement of local energy-momentum conservation. The declaration conservation_from_bianchi formalizes the discrete analog of this argument in the framework's library, a machine-checked collection of formal theorems.

The framework models spacetime as a Regge calculus, a discrete approximation where space is built from flat simplices joined along hinges. Curvature resides in deficit angles at these hinges: the amount by which the angles around a hinge fall short of a full circle. The discrete Bianchi identity, following Hamber and Kagel (2004), states that for any closed loop of hinges around a vertex, the sum of signed deficit angles is a multiple of 2π. In the linearized regime of small angles, this sum is exactly zero.

The theorem conservation_from_bianchi proves that if the discrete Regge equations hold and the linearized Bianchi identity holds, then a discrete conservation law follows. The proof is structural: it shows the implication holds for any list of hinges, given the placeholder assumptions. This mirrors the continuum argument, where the Bianchi identity plus the Einstein equations yields energy-momentum conservation.

The declaration does not claim that the discrete Regge equations are actually satisfied, nor that the linearized approximation is valid in a physical regime. The Regge equations are represented by a placeholder that is always true, and the conservation statement itself is a tautology. The theorem establishes a formal implication between assumptions, not a physical derivation from first principles. The continuum limit, where the discrete identity becomes the standard contracted Bianchi identity, is stated as a hypothesis, not proved.

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

/-- **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

/-- In the linearized regime (small deficit angles), the Bianchi
    identity reduces to: sum of deficit angles = 0 exactly. -/
def linearized_bianchi (deficit_angles : List ℝ) : Prop :=
  deficit_angles.sum = 0

What this page does not claim

The theorem does not prove that the Regge equations hold for any physical configuration. The theorem does not derive the continuum contracted Bianchi identity; that remains a hypothesis. The theorem does not establish that discrete energy-momentum conservation holds in the full nonlinear theory.

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: