Gravity Regge Calculus Deficit Neg Of Angle Excess

The sign of curvature

Regge calculus, introduced by Tullio Regge in 1961, is a way to do general relativity without smooth spacetime. It replaces the continuous fabric of space and time with a patchwork of flat building blocks, usually triangles and tetrahedra, glued together along their faces. All the curvature that would have been spread smoothly through spacetime is concentrated along the lower-dimensional seams where several blocks meet. The amount of curvature at such a seam is measured by a deficit angle: the angle you get when you add up all the dihedral angles of the blocks surrounding the seam and subtract the result from 2π, the angle of a full turn.

The sign of that deficit angle is the sign of the curvature. If the blocks around a seam use up less than a full turn, the deficit is positive, and the space curves like the inside of a sphere. If they use up more than a full turn, the deficit is negative, and the space curves like a saddle. The theorem deficit_neg_of_angle_excess in the framework's machine-checked library of formal theorems states exactly this second case: for any hinge, if the sum of its surrounding dihedral angles is greater than 2π, then its deficit angle is strictly less than zero. Its counterpart, deficit_pos_of_angle_deficit, states the first case: if the sum is less than 2π, the deficit is strictly positive. The proofs are one-line arithmetic consequences of the definition of a deficit angle.

The framework's library also proves the flat case: a regular cubic lattice, where four right angles meet at every edge, has a deficit angle of exactly zero, and the total Regge action vanishes. These three results together give a complete sign table for curvature on a piecewise-flat lattice. They certify that the discrete geometry behaves the way smooth geometry does: positive curvature where angles close up, negative where they open out, and none where they balance.

In Recognition Science, this sign table is a piece of the discrete gravity programme. The framework models the lattice as Z³ × Z, and the edge lengths are set by a field derived from its cost function. The theorem itself, however, is purely geometric. It does not depend on the cost function, on the golden ratio, or on any other RS-specific constant. It is a statement about any list of angles that sums past a full turn. What the framework adds is the claim that this geometry is the one its cost function forces, a claim that rests on the separate forcing chain, not on this theorem.

/-- Deficit angle is negative when total angle > 2*pi (negative curvature). -/
theorem deficit_neg_of_angle_excess (h : HingeData)
    (h_more : 2 * Real.pi < h.dihedral_angles.sum) :
    deficit_angle h < 0 := by
  unfold deficit_angle; linarith

/-- Deficit angle is positive when total angle < 2*pi (positive curvature). -/
theorem deficit_pos_of_angle_deficit (h : HingeData)
    (h_less : h.dihedral_angles.sum < 2 * Real.pi) :
    0 < deficit_angle h := by
  unfold deficit_angle; linarith

/-- On the flat cubic lattice Z^3, each edge is shared by 4 cubes.
    Each cube contributes dihedral angle pi/2.
    Sum = 4 * pi/2 = 2*pi, so deficit = 0. -/
theorem cubic_lattice_flat :
    2 * Real.pi - 4 * (Real.pi / 2) = 0 := by ring

What this page does not claim

This theorem does not claim that the RS cost function produces these edge lengths; that is a separate, open bridge. This theorem does not claim anything about the total Regge action for non-flat configurations. This theorem does not claim that a negative deficit angle corresponds to a specific cosmological or astrophysical phenomenon.

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/ReggeCalculus.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: