Gravity Discrete Bianchi Flat Bianchi

The flat case

The Bianchi identity is a central result in general relativity: a geometric condition, nabla^mu G_mu_nu = 0, that follows from the symmetries of the Riemann tensor and, when combined with the Einstein field equations, forces the conservation of energy and momentum. In the discrete setting of Regge calculus, where spacetime is approximated by flat simplices glued along hinges, Hamber and Kagel (2004) formulated an exact analog: the product of rotation matrices (holonomies) around any contractible loop must return to the identity. For a loop of hinges sharing a vertex, this means the sum of signed deficit angles equals zero modulo 2π.

The declaration flat_bianchi in the machine-checked library of formal theorems proves the simplest possible case of this discrete identity. It states: if every deficit angle in a list is exactly zero, then their sum is zero. This is a statement about a list of real numbers, established by induction. It is true by definition, and it confirms that a flat lattice, with no curvature at any hinge, trivially satisfies the discrete Bianchi identity. The proof is a direct computation, not a deep geometric insight.

In Recognition Science, this statement is part of a larger structure. The framework models reality as a discrete ledger of recognition events, and it derives physical constants and dimensional structure from a forced cost function. Within that framework, the discrete Bianchi identity is a bridge: it connects the geometric consistency of a discrete spacetime to the conservation of a discrete stress-energy. The flat_bianchi statement is a small but necessary brick in that bridge, showing that the identity holds in the absence of curvature.

What flat_bianchi does not claim is more interesting. It does not prove that a flat lattice is the only solution, nor that any physical spacetime is flat. It says nothing about the continuum limit, where the discrete identity is hypothesized to become the familiar contracted Bianchi identity; that step is explicitly marked as a hypothesis, not a proven result. It does not establish the discrete conservation law, which requires the Regge equations to hold and is only a placeholder in the current formalization. And it does not, on its own, force any physical conclusion about gravity or spacetime. It is a lemma about zeros, a necessary but modest foundation.

The real content of the discrete Bianchi identity lives elsewhere: in the constraint it places on deficit angles at shared edges, and in the conservation law that follows when combined with the Regge equations. The flat case is the sanity check that the identity is not vacuous, that a world without curvature is consistent. It is the zero on the number line, not the number line itself.

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

/-- **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 continuum limit, the discrete Bianchi identity becomes
    the contracted Bianchi identity: nabla^mu G_mu_nu = 0.

    The key steps (not fully formalized here):
    1. Discrete holonomy around a plaquette -> Riemann tensor
    2. Discrete Bianchi (holonomy around contractible loop = 1)
       -> algebraic Bianchi R_{[mu nu rho]sigma} = 0
    3. Contract -> nabla^mu G_mu_nu = 0

    We state this as a hypothesis for the continuum limit. -/
def H_bianchi_continuum_limit : Prop :=
  ∀ (deficit_angles : List ℝ),
    linearized_bianchi deficit_angles →
    True  -- Represents: nabla^mu G_mu_nu = 0 in the continuum

What this page does not claim

The theorem does not prove that any physical spacetime is flat or that flatness is the only consistent state. The theorem does not establish the discrete conservation law, which requires the Regge equations to hold. The theorem does not derive the continuum Bianchi identity, which remains an explicit hypothesis.

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: