Geometry Regge Action Concrete Canonical Edge Stencil Dirichlet Energy Nonneg

The edge stencil energy

In the finite-element study of curved spacetime, the Regge action approximates the Einstein-Hilbert action of general relativity by replacing smooth geometry with a triangulated one. The action is built from the deficit angles around the hinges (edges) of the triangulation. When the geometry is perturbed by scaling the vertices, the second variation of this action defines a Hessian matrix, whose quadratic form measures the energy cost of a small deformation. In the Recognition Science framework's machine-checked library of formal theorems, the declaration canonicalEdgeStencilDirichletEnergy_nonneg proves a specific property of one such energy expression.

That expression, the canonical edge stencil Dirichlet energy, is a sum over every edge in the triangulation. For each edge, it takes the square root of the edge's squared length, multiplies it by the square of the difference of the deformation values at the edge's two endpoints, and adds the result. The theorem states that this sum is always greater than or equal to zero, for any consistent triangulation and any vertex deformation. The proof is a direct one: each term in the sum is a product of a nonnegative number (the square root of a length) and a square, so each term is nonnegative, and a sum of nonnegative terms is nonnegative. This is a formal, machine-checked result in the framework's library.

The significance of this nonnegativity is that it identifies the edge stencil energy as a genuine measure of deformation cost. In the framework's account, this energy is shown to equal the quadratic form of the canonical Regge Hessian, and that Hessian's quadratic form is proven nonnegative as a consequence. This means that the second-order variation of the Regge action under vertex scaling is never negative, so the flat configuration sits at a local minimum of the action. The theorem is a structural guarantee about the discrete geometry, not a statement about the physical universe.

The declaration does not claim that the full Regge action is convex, nor that the remainder term in its Taylor expansion vanishes or is bounded. It does not claim that the energy is positive definite, only nonnegative; a constant deformation gives zero energy. It also does not claim that the edge stencil energy equals the canonical Dirichlet energy in general; that equality is a separate theorem requiring additional conditions about the sum over edges and the reindexing of vertex pairs. The nonnegativity result is a local, algebraic fact about one specific energy expression.

theorem canonicalEdgeStencilDirichletEnergy_nonneg
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    0 ≤ canonicalEdgeStencilDirichletEnergy K hK ξ := by
  unfold canonicalEdgeStencilDirichletEnergy
  refine Finset.sum_nonneg ?_
  intro e _
  exact mul_nonneg (Real.sqrt_nonneg _) (sq_nonneg _)

theorem canonicalEdgeStencilDirichletEnergy_nonneg
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (ξ : VertexPotential K) :
    0 ≤ canonicalEdgeStencilDirichletEnergy K hK ξ := by
  unfold canonicalEdgeStencilDirichletEnergy
  refine Finset.sum_nonneg ?_
  intro e _
  exact mul_nonneg (Real.sqrt_nonneg _) (sq_nonneg _)

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 ξ

What this page does not claim

The full Regge action is convex or that its Taylor remainder vanishes. The edge stencil energy is positive definite, only nonnegative. The edge stencil energy equals the canonical Dirichlet energy without additional conditions.

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: