Geometry Regge Action Nonlinear Hessian Proof

The nonlinear Hessian proof

The Regge action is a way to write general relativity on a triangulated space, a space built from flat tetrahedra joined along triangular faces. The action is a sum over the edges, or hinges, of the tetrahedra. Each term multiplies the length of an edge by the deficit angle there, the angle by which the surrounding tetrahedra fail to lie flat. This discrete formulation was introduced by Tullio Regge in 1961 as a tool for numerical relativity.

A natural question is whether this discrete action behaves like its continuum cousin under small perturbations. In the continuum, the Einstein-Hilbert action has a second variation at flat space that is a quadratic form in the metric perturbation. The discrete analogue asks: if you move the vertices of the triangulation slightly away from a flat configuration, does the second derivative of the Regge action match the quadratic form you get from the standard linearized theory? That matching is what the nonlinear Hessian proof establishes.

The proof works by taking a one-parameter family of vertex positions, a line through the flat configuration in the space of all triangulations. Along such a line, the action becomes a function of one variable. The theorem states that the second derivative of this function at zero, where the configuration is flat, equals the Hessian quadratic form of the canonical linearized Regge action evaluated on the same direction. In symbols, for any direction ξ, the second derivative of the action along the line equals (1/2) times the Hessian quadratic form H(ξ, ξ).

In Recognition Science, this result is part of a larger program that derives physical structure from a discrete ledger of recognition events. The framework models spacetime as a triangulation whose geometry is determined by the edge lengths, and the Regge action is the natural cost functional on that geometry. The proof that the nonlinear action reduces to the canonical quadratic form at flat space is a consistency check: it shows the discrete theory has the correct linearized limit, the same limit that connects general relativity to its weak-field approximation.

The machine-checked library of formal theorems contains the full argument. The central statement, NonlinearReggeDirectionalHessianTheorem, is a definition that asserts the second derivative condition. The library proves this theorem from a chain of intermediate results: differentiability of the hinge measure and deficit angle along the line, a product rule for the derivative of the action, and a chain rule for the conformal Schlaefli angle squared. The final step reduces the problem to showing that a remainder term, the difference between the nonlinear action and its quadratic approximation, has zero second variation at flat space. That remainder reduction is itself a proved equivalence in the library.

/-- Exact second-directional-variation statement for the full nonlinear Regge
action. -/
def NonlinearReggeDirectionalHessianTheorem
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∀ ξ : VertexPotential K,
    HasSecondDerivAt (actionAlongLine K hK ξ)
      (hessianQuadratic (canonicalReggeHessian K hK) ξ) 0

theorem remainder_reduction_eq_canonicalRemainderSecondVariation
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    NonlinearReggeHessianReducedToRemainder K hK ↔
      CanonicalRemainderSecondVariationZero K hK := by
  rfl

theorem hingeDeficitLineDifferentiabilityNearZero_of_flatConfiguration
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hFlat : FlatConfiguration K hK) :
    HingeDeficitLineDifferentiabilityNearZeroTarget K hK := by
  intro ξ
  rw [Filter.eventually_all]
  intro e
  have hHinge :=
    differentiableAt_eventually_of_contDiffAt_top
      (fun t : ℝ => hingeMeasureUnderConformal K hK (linePotential K ξ t) e) 0
      (hingeLine_contDiffAt_zero K hK ξ e)
  have hDef :=
    differentiableAt_eventually_of_contDiffAt_top
      (fun t : ℝ => deficitAngle K (linePotential K ξ t) e) 0
      (deficitLine_contDiffAt_zero_of_flatConfiguration K hK hFlat ξ e)
  filter_upwards [hHinge, hDef] with t htHinge htDef
  exact ⟨htHinge, htDef⟩

What this page does not claim

The proof does not establish the Regge action as the unique discretization of general relativity. The theorem does not apply to arbitrary configurations, only to flat ones. The module does not prove that the Regge action itself is derived from the recognition ledger.

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