Gravity Regge Calculus Regge Action Flat

The flat-space check

Regge calculus, introduced by Tullio Regge in 1961, is a way to do general relativity without smooth geometry. It replaces the continuous fabric of spacetime with a patchwork of flat, four-dimensional triangles called simplices. Curvature is not spread out; it is concentrated along the shared edges, or hinges, where the simplices meet. The amount of curvature at a hinge is measured by a deficit angle: the angle by which the surrounding flat pieces fail to close up around that edge. The Regge action, the quantity whose behavior governs the dynamics, is the sum over all hinges of the hinge's area times its deficit angle.

The Recognition Science framework uses this machinery on a specific lattice, a regular grid of points in space and time. The declaration regge_action_flat proves a sanity check that any such construction must pass. It states that if every hinge in the list has a deficit angle of exactly zero, meaning the flat pieces fit together perfectly with no curvature anywhere, then the total Regge action is exactly zero. This is the discrete analogue of saying that flat space has zero action, a requirement for the theory to reduce to the correct classical limit. The proof is a direct calculation: each term in the sum is an area multiplied by zero, so the whole sum vanishes.

The declaration is part of a larger, machine-checked library of formal theorems. The library also proves that a simple cubic lattice, where four right angles meet at each vertex, has zero deficit angle, confirming that the familiar flat grid is indeed flat. It further shows that a positive deficit angle corresponds to a shortage of angle around a hinge, and a negative one to an excess, matching the geometric intuition that positive curvature means angles sum to less than a full turn. These results are collected in a certificate structure that bundles the key properties of the Regge calculus setup.

In Recognition Science, this flat-space check is a foundation, not a destination. It validates that the discrete geometry is internally consistent before the framework uses it to model gravity. The declaration does not, however, claim that this lattice is the true structure of spacetime, nor does it derive the equations of motion that would tell the edge lengths how to evolve. It is a necessary condition for a sensible theory, not a complete one.

/-- The Regge action vanishes for flat configurations. -/
theorem regge_action_flat (hinges : List HingeData)
    (h_flat : ∀ h ∈ hinges, deficit_angle h = 0) :
    regge_action hinges = 0 := by
  unfold regge_action
  suffices h : (hinges.map (fun h => h.area * deficit_angle h)) = hinges.map (fun _ => 0) by
    rw [h]; simp
  apply List.map_congr_left
  intro h hm
  rw [h_flat h hm, mul_zero]

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

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

What this page does not claim

This declaration does not claim that the Z^3 by Z lattice is the actual structure of physical spacetime. It does not derive the dynamical equations that determine how the edge lengths evolve. It does not prove that the Regge action is the unique or final action for discrete gravity in the framework.

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: