Geometry Regge Action Concrete Canonical Regge Hessian Quadratic Nonneg

The stability of the Regge action

The Regge action is a way to write gravity as a sum over a triangulated space, a grid of flat tetrahedra glued together. In 1961, Tullio Regge proposed this discrete formulation to make general relativity computable. The action measures the total curvature of the grid: for each edge, it multiplies the edge's length by the deficit angle, the amount by which the surrounding tetrahedra fail to lie flat. This sum approximates the Einstein-Hilbert action of smooth spacetime when the grid is fine.

A central question for any action is whether small changes in the geometry increase or decrease the action. If the action decreases, the configuration is unstable and the theory is physically suspect. The declaration canonicalReggeHessian_quadratic_nonneg in the framework's machine-checked library of formal theorems proves that, under a specific conformal ansatz, the quadratic part of the action's variation is always nonnegative. In plain terms: the action has no direction in which it curves downward. The second variation, the Hessian quadratic form, is positive semidefinite.

The proof works by showing that the Hessian quadratic form equals a canonical Dirichlet energy, a sum over edges of a positive weight times the squared difference of vertex potentials. Each term is a square, hence nonnegative, and the sum of nonnegative terms is nonnegative. The theorem holds for any finite 3D triangulation that is incidence-consistent, meaning the edge data is consistently defined. The result is a theorem in the framework's library, proved in the Lean proof assistant with no additional axioms beyond the standard logical ones.

In Recognition Science, this theorem is a concrete step in a larger program. The framework models physical structure from a ledger of recognition events, and it derives constants like the golden ratio and three spatial dimensions from a forcing chain. Here, the Regge action supplies the classical gravitational dynamics on a discrete grid. The nonnegativity result establishes that the conformal Regge action is locally stable, a necessary condition for it to serve as a physically viable starting point for a discrete theory of gravity.

The theorem does not claim that the full Regge action is convex, only its quadratic part under the conformal ansatz. It does not address the existence or uniqueness of a global minimum, nor does it prove that the discrete theory converges to smooth general relativity in any continuum limit. The result is a local stability statement, not a complete theory of quantum gravity. It is one verified piece of a much larger, still unfinished structure.

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]

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 ξ

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

What this page does not claim

The full Regge action is convex or has a unique global minimum. The discrete theory converges to smooth general relativity in any continuum limit. The theorem provides a complete theory of quantum gravity. The conformal ansatz covers all possible metric variations.

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: