Geometry Regge Hessian3 D Regge Hessian Data

The Hessian interface

The Regge action is a discrete version of Einstein's theory of gravity, defined on a space built from flat triangular pieces glued together. In three dimensions, the pieces are tetrahedra, and the geometry is encoded in their edge lengths. The action assigns a number to each such triangulated space, and its second variation, the Hessian, controls how that number bends when you perturb the edge lengths. The declaration ReggeHessianData is a formal contract: it bundles an action, a Hessian matrix, and the theorem that the matrix really is the quadratic Taylor coefficient of the action.

The contract is stated under a conformal ansatz, meaning the perturbation is not arbitrary but scales each vertex by a real number, a conformal potential. The structure declares four fields. First, an action, a function from vertex potentials to real numbers. Second, a Hessian, a matrix of second derivatives at zero potential. Third, a symmetry condition, the matrix equals its transpose. Fourth, a second-variation identity: for every perturbation, the change in the action equals one half times the Hessian quadratic form applied to the perturbation. The theorem regge_secondVariation_eq_hessian extracts that identity as a standalone statement.

What the declaration does not do is compute the Hessian for any particular triangulation. It provides the interface, not the numbers. A concrete implementation must supply the action, the matrix, and a proof that the identity holds. The symmetry condition is declared as data, not derived. The first variation being zero is declared as a proposition, flat_firstVariation_zero, with no proof attached. The framework's library of formal theorems, a machine-checked collection, establishes the interface and the extraction theorem, but it leaves the analytic work of building a specific Regge package to future modules.

In plain terms, this is a precise vocabulary for talking about the second variation of discrete gravity. It forces any implementation to state its action, its Hessian, and the relationship between them in one place, checked by the kernel. The payoff is that when a concrete package appears, its claim to be the genuine Regge Hessian is auditable: the identity must hold for every perturbation, not just at a point. That is the difference between naming a matrix and proving it is the Hessian.

/-- Genuine Regge Hessian data for a triangulation.  `action` is the
Regge action under the conformal ansatz, and `hessian` is the matrix of
its second variation at `ξ = 0`. -/
structure ReggeHessianData (K : Triangulation3D) where
  action : VertexPotential K → ℝ
  hessian : Fin K.nV → Fin K.nV → ℝ
  hessian_symm : ∀ i j, hessian i j = hessian j i
  flat_firstVariation_zero : Prop
  secondVariation :
    ∀ ξ : VertexPotential K,
      action ξ - action (zeroPotential K) =
        (1 / 2) * hessianQuadratic hessian ξ

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

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

/-- Genuine Regge Hessian data for a triangulation.  `action` is the
Regge action under the conformal ansatz, and `hessian` is the matrix of
its second variation at `ξ = 0`. -/
structure ReggeHessianData (K : Triangulation3D) where
  action : VertexPotential K → ℝ
  hessian : Fin K.nV → Fin K.nV → ℝ
  hessian_symm : ∀ i j, hessian i j = hessian j i
  flat_firstVariation_zero : Prop
  secondVariation :
    ∀ ξ : VertexPotential K,
      action ξ - action (zeroPotential K) =
        (1 / 2) * hessianQuadratic hessian ξ

What this page does not claim

No specific Hessian matrix is computed for any triangulation. The first variation being zero is asserted as a proposition, not proved. The declaration does not establish that the Regge action is the unique discrete gravity action.

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: