Geometry Regge Hessian3 D Vertex Potential

Vertex potential in 3D

A vertex potential is a simple bookkeeping object: it assigns a real number to each vertex of a finite 3D triangulation. Think of a triangulated surface like a geodesic dome, then add a third dimension so the shape is filled with tetrahedra. The potential is just a label on each corner, a real number that can vary freely. The framework's declaration VertexPotential defines this as a function from the set of vertices to the real numbers, nothing more.

The zero potential, which assigns 0 to every vertex, serves as the flat baseline. The framework then builds a quadratic form from a Hessian matrix, a standard way to measure curvature near a point. The key structure is ReggeHessianData: it packages the Regge action, its Hessian matrix, a symmetry condition, and a theorem stating that the action's second variation equals half the quadratic form. This is the analytic core: the framework proves that the quadratic Taylor coefficient is represented by that matrix, a theorem named regge_secondVariation_eq_hessian.

This matters because the Regge action is a discrete version of general relativity's Einstein-Hilbert action, used in numerical relativity and quantum gravity. The framework provides a machine-checked interface for studying its second variation in three dimensions. The declaration establishes the vocabulary: what a vertex potential is, what the zero potential is, and how the Hessian connects to the action's curvature. It does not claim that any particular triangulation is physical, nor that the Regge action itself is derived from first principles here.

In Recognition Science, this sits within a broader program of deriving physical structure from a forced cost function. The framework models the Regge action under a conformal ansatz, where edge lengths scale by vertex potentials. The declaration is a definitional choice, not a theorem about physics. It sets up the language for studying how the action responds to conformal variations at vertices, a tool for exploring the discrete geometry of spacetime.

/-- Vertex conformal potentials on a finite 3D triangulation. -/
abbrev VertexPotential (K : Triangulation3D) := Fin K.nV → ℝ

/-- Extract the second-variation formula from a concrete Hessian package. -/
theorem regge_secondVariation_eq_hessian
    (K : Triangulation3D) (D : ReggeHessianData K) (ξ : VertexPotential K) :
    D.action ξ - D.action (zeroPotential K) =
      (1 / 2) * hessianQuadratic D.hessian ξ :=
  D.secondVariation ξ

What this page does not claim

The declaration does not prove that any specific triangulation is physically realized. It does not derive the Regge action from the framework's cost function. It does not establish that the Hessian matrix is positive definite or that the action has a minimum.

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/ReggeHessian3D.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: