Gravity Discrete Bianchi Linearized Implies General

A bridge between small and full curvature

A discrete version of a central geometric identity in gravity, the Bianchi identity, holds exactly when a simpler linearized form holds. The declaration linearized_implies_general in the framework's machine-checked library of formal theorems proves that if the sum of small deficit angles around a closed loop is zero, then the full discrete Bianchi identity holds. In plain terms: when curvature is weak, the exact constraint on how space bends around a point is already captured by the linear approximation.

The classical background is Regge calculus, a discrete formulation of general relativity where space is built from flat simplices joined along hinges. Curvature lives at these hinges as a deficit angle, the amount by which the flat pieces fail to close around a shared edge. The continuum Bianchi identity, nabla^mu G_mu_nu = 0, is a geometric consequence of the Riemann tensor symmetries; together with the Einstein equations it forces energy-momentum conservation. The discrete analog, following Hamber and Kagel (2004), states that the product of rotation matrices (holonomies) around any contractible loop is the identity, equivalently that signed deficit angles around a closed loop sum to zero modulo 2*pi.

The theorem bridges two regimes. The general identity allows the sum of deficit angles to equal any integer multiple of 2*pi, reflecting that a loop can wind around a vertex. The linearized version demands the sum be exactly zero, appropriate for small angles where higher-order winding is negligible. The proof is a one-line construction: given the linearized hypothesis, choose the integer n = 0 in the general definition. This is not a physical approximation; it is a formal implication between two definitions, verified by the kernel of the proof assistant.

In Recognition Science, this theorem is part of a broader program that derives physical structure from a discrete ledger of recognition events. The framework models gravity as a discrete system where curvature is encoded in deficit angles, and this declaration is one step in showing that the discrete geometry satisfies the same conservation laws as the continuum. The library also contains a structural theorem that conservation follows from the discrete Bianchi identity combined with the Regge equations, though the placeholder for the Regge equations themselves is not yet filled in.

What the declaration does not claim is equally important. It does not prove that the linearized regime is physically realized, nor that the continuum limit of the discrete theory reproduces general relativity. The bridge to the continuum contracted Bianchi identity is stated as a hypothesis, not a theorem. The declaration is a statement about the relationship between two definitions inside the framework, not a claim about the empirical world.

/-- 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]⟩

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

What this page does not claim

The theorem does not assert that the linearized regime is physically realized or that small deficit angles occur in any particular spacetime. The declaration does not prove that the continuum limit of the discrete theory reproduces general relativity; that bridge is a hypothesis. The theorem does not establish the Regge equations themselves, which appear only as a placeholder in the conservation statement.

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: