Gravity Discrete Bianchi Discrete Bianchi Cert

The discrete Bianchi certificate

The Bianchi identity is a geometric fact about curved spacetime: the divergence of the Einstein tensor is identically zero. In general relativity, this identity, combined with Einstein's field equations, forces the local conservation of energy and momentum. The Recognition Science library formalizes the discrete analog of this fact for Regge calculus, a lattice approach to gravity where spacetime is built from flat simplices and curvature is concentrated along hinges (edges in three dimensions).

The certificate discrete_bianchi_cert is a machine-checked collection of formal theorems. It establishes three results. First, for a flat lattice, where all deficit angles are zero, the linearized Bianchi identity holds trivially. Second, the linearized identity, where the sum of deficit angles around a vertex equals zero exactly, implies the more general identity, where the sum equals an integer multiple of 2π. Third, if the Regge equations hold and the linearized Bianchi identity holds, then a discrete conservation law follows, mirroring the continuum result.

The core geometric statement is the discrete Bianchi identity itself: the sum of signed deficit angles around any closed loop of hinges sharing a common vertex equals zero modulo 2π. This is the discrete analog of the statement that the product of rotation matrices (holonomies) around a contractible loop is the identity. In the small-angle limit, this becomes an exact sum to zero. The certificate packages these theorems into a single structure, providing a formal guarantee of their consistency.

In Recognition Science, this certificate is a building block. It provides a rigorous, machine-checked foundation for the discrete geometry of gravity. The certificate does not claim to derive the continuum limit, nor does it claim that the Regge equations themselves are satisfied by any particular physical configuration. It only proves the logical relationship between the geometric identity and the conservation law, given the stated assumptions.

/-- For a flat lattice, all deficits are zero, so Bianchi is trivially satisfied. -/
theorem flat_bianchi (deficits : List ℝ) (h : ∀ d ∈ deficits, d = 0) :
    linearized_bianchi deficits := by
  unfold linearized_bianchi
  induction deficits with
  | nil => simp
  | cons a as ih =>
    simp only [List.sum_cons]
    have ha : a = 0 := h a (List.mem_cons_self ..)
    rw [ha, zero_add]
    exact ih (fun d hd => h d (List.mem_cons_of_mem _ hd))

/-- The linearized Bianchi identity implies the general one (with n = 0). -/
theorem linearized_implies_general (deficits : List ℝ)
    (h : linearized_bianchi deficits) :
    discrete_bianchi_identity deficits :=
  ⟨0, by unfold linearized_bianchi at h; simp [h]⟩

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

What this page does not claim

The certificate does not prove that the continuum limit of the discrete Bianchi identity is the contracted Bianchi identity, which is stated as a hypothesis. The certificate does not prove that any particular physical configuration satisfies the Regge equations. The certificate does not establish that the discrete conservation law is equivalent to the continuum energy-momentum conservation.

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: