Geometry Regge Action Concrete

The concrete Regge action

The Regge action is a way to do general relativity without smooth manifolds. Instead of a continuous curved spacetime, one uses a flat 3D triangulation: a network of tetrahedra glued together. Curvature is concentrated along the edges, or hinges, where the tetrahedra meet. The action is a sum over these hinges of the hinge's length times the deficit angle, which measures how much the surrounding tetrahedra fail to lie flat. This discrete formulation, introduced by Tullio Regge in 1961, is the standard starting point for numerical relativity and quantum gravity.

In Recognition Science, this construction is examined with a precise question: when you scale the length of each edge by a factor that depends on the two vertices it connects, what is the second-order change in the action? The scaling is written as exp(ξ_u + ξ_v), where ξ is a potential assigned to each vertex. The answer, proved in a machine-checked library, is that the action decomposes into a constant term, a quadratic form in ξ, and a remainder. The quadratic form is the Hessian of the action. The library proves that this Hessian is symmetric, that its row sums are zero, and that the quadratic form it defines is non-negative.

The non-negativity is the key result. It means the second-order change in the action is always greater than or equal to zero, so the flat configuration is a local minimum of the action. The proof identifies the Hessian's quadratic form with a canonical Dirichlet energy, a sum over edges of the squared difference in the vertex potential, weighted by the edge length. This is a discrete analogue of the familiar fact that the Laplacian is a positive operator. The library also proves that this Dirichlet energy can be written as a sum over edges directly, which is the concrete form of the stencil used in numerical simulations.

The main theorem, genuineReggeHessianTarget, states that for every incidence-consistent triangulation, there exists a concrete second-order data structure. This is what it means to make the Regge action concrete: the abstract existence of a Hessian is replaced by a specific, computable formula. The theorem is proved by constructing the data from the canonical Hessian defined in the library. This bridges the gap between the abstract theory of the Regge action and the concrete numerical objects needed to compute with it.

What this establishes, in plain language, is that the discrete geometry of Regge calculus is well-behaved at second order. The flat configuration is a stable minimum, the second-order response is computable from a simple edge-based formula, and all of this is guaranteed by a machine-checked proof. This is a necessary foundation for any attempt to quantize the theory, where the Hessian plays the role of the kinetic term. The library does not itself provide a quantum theory, but it provides the classical input that a quantum theory would need.

In the framework of Recognition Science, this concrete Regge action is a step toward deriving the structure of space from the cost of recognition. The framework's forcing chain derives three spatial dimensions from a discrete ledger of events; this library provides the geometric machinery to describe how that discrete space curves. The connection between the two is a target for future work, not a result of this library.

/-- The concrete 3D Regge action under the vertex-conformal ansatz. -/
def reggeAction
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) : ℝ :=
  ∑ e : Fin K.nE,
    hingeMeasureUnderConformal K hK ξ e * deficitAngle K ξ e

/-- Exact decomposition of the nonlinear action into its value at zero, a
candidate quadratic Hessian term, and the remaining nonlinear part. -/
theorem reggeAction_taylor_decomposition
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (H : Fin K.nV → Fin K.nV → ℝ)
    (ξ : VertexPotential K) :
    reggeAction K hK ξ =
      reggeAction K hK (zeroPotential K) +
        (1 / 2) * hessianQuadratic H ξ +
        reggeActionRemainder K hK H ξ := by
  unfold reggeActionRemainder
  ring

theorem canonicalReggeHessian_quadratic_nonneg
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    0 ≤ hessianQuadratic (canonicalReggeHessian K hK) ξ := by
  rw [canonicalReggeHessian_quadratic_eq_dirichlet]
  exact canonicalDirichletEnergy_nonneg K hK ξ

theorem canonicalReggeHessian_quadratic_eq_dirichlet
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    hessianQuadratic (canonicalReggeHessian K hK) ξ =
      canonicalDirichletEnergy K hK ξ := by
  rw [canonicalReggeHessian_quadratic_expanded,
    canonicalDirichletEnergy_expanded]

/-- The genuine Hessian target is discharged for the canonical second-order
incidence Regge data. -/
theorem genuineReggeHessianTarget : GenuineReggeHessianTarget := by
  intro K hK
  exact ⟨canonicalReggeSecondOrderData K hK⟩

What this page does not claim

This library does not prove that the Regge action converges to the Einstein-Hilbert action in any continuum limit. This library does not provide a quantum theory of gravity; it only establishes the classical second-order structure. The connection between this concrete Regge action and the framework's derivation of three spatial dimensions is not established here.

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/Geometry/ReggeActionConcrete.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: