Geometry Regge Action Concrete Canonical Regge Hessian Quadratic Eq Dirichlet

The quadratic identity

Regge calculus is a discrete approach to general relativity where spacetime is approximated by a mesh of flat tetrahedra. The Regge action, a sum over edges of the edge length times the deficit angle, measures the total curvature concentrated along the hinges of this mesh. For small variations of the vertex positions, the action changes; its second variation, the Hessian, controls the stability and dynamics of the discrete geometry.

The declaration canonicalReggeHessian_quadratic_eq_dirichlet establishes a clean structural fact about this second variation. Under a conformal ansatz, where each edge length scales by the exponential of the sum of its two endpoint potentials, the Hessian's quadratic form is exactly equal to a canonical Dirichlet energy. That energy is a sum over all edges of the edge length times the squared difference of the potentials at its endpoints. In symbols, for any vertex potential ξ, the identity reads: hessianQuadratic(canonicalReggeHessian K hK) ξ = canonicalDirichletEnergy K hK ξ.

This identity is proved in the framework's machine-checked library of formal theorems for any finite 3D triangulation with consistent incidence data. It is not a numerical approximation; it is an exact equality of algebraic expressions. The proof relies on expanding both the Hessian and the Dirichlet energy into sums over vertex pairs and then reindexing those sums, a step that requires the triangulation to have no self-loop edges. The result is a bridge between the geometric action and a simpler, purely combinatorial energy.

In Recognition Science, this bridge is a stepping stone. The framework models the Regge action's second variation as a Dirichlet form, which is a standard object in the theory of discrete Laplacians and random walks. This connection suggests that the dynamics of the discrete geometry can be studied through the spectral properties of a weighted graph Laplacian. The identity also immediately implies that the Hessian's quadratic form is non-negative, a stability condition, and that its row sums are zero, a conservation property tied to the invariance of the action under constant shifts of the potential.

What the declaration does not claim is that the Regge action itself is equal to the Dirichlet energy. The identity holds only for the second variation, not for the full action, which includes a remainder term. Nor does it claim that the Hessian is the Dirichlet energy for all variations; the conformal ansatz is a specific restriction on how the geometry can change. The result is a precise, conditional statement about a particular quadratic form, not a global equivalence of actions.

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_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 ξ

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

What this page does not claim

The Regge action itself equals the Dirichlet energy. The identity holds for variations outside the conformal ansatz. The declaration proves anything about the physical viability of Regge calculus as a theory of quantum gravity.

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: