Geometry Regge Action Second Variation

The Second Variation

The Regge action is a way to write the cost of curvature for a space built from flat triangular pieces, the kind of discrete geometry used in numerical relativity. In the Recognition Science framework, this action is not a free choice: it is forced by the same cost structure that fixes the golden ratio and the number of spatial dimensions. The second variation of that action is the quadratic term in its Taylor expansion, the part that describes how the cost responds to small bending of the vertex positions away from a flat configuration.

Classically, the second variation of an action is the object that decides stability: a minimum of the action has a positive second variation, so small perturbations cost energy and the configuration holds. For the Regge action, the second variation is a Hessian, a matrix indexed by pairs of vertices, and its quadratic form measures the cost of a small displacement pattern. The standard result, due to Regge in 1961, is that this Hessian controls the linearized dynamics of the discrete geometry.

In Recognition Science, the module ReggeActionSecondVariation.lean states the target precisely. It defines a one-parameter line through the flat potential, a straight path in the space of vertex displacements, and asks how the action changes along that line. The central claim, CanonicalHessianSecondVariationAtZero, says that the second derivative of the action along any such line equals the quadratic form of the canonical Hessian, the one built from the incidence structure of the triangulation. That is the statement that the nonlinear action has the expected quadratic behavior at flatness.

The module also handles the remainder. After subtracting the quadratic term, what is left should be cubic or higher in the displacement size. The definition LocalCubicRemainderBound states that this remainder is bounded by a constant times the cube of the displacement norm, at least for small displacements. A theorem packages this as a usable input: if the remainder is identically zero, the bound holds with constant zero, a sanity check that the definitions are consistent.

What this establishes in plain language is a clean separation. The second variation of the Regge action is exactly the canonical Hessian, and everything beyond that is at least cubic. That means the quadratic approximation of the action is controlled by the incidence structure alone, and the nonlinear corrections do not spoil the local picture. This is the discrete analogue of the classical statement that the second variation of the Einstein-Hilbert action is the linearized Einstein operator, and it is the foundation for stability arguments in the framework's discrete geometry.

/-- Phase-D second-variation theorem, conditional on the named nonlinear
second-variation input. -/
theorem reggeAction_secondVariation_eq_canonicalHessian
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_flat : FlatConfiguration K hK)
    (h_second : ReggeActionSecondVariationInput K hK h_flat) :
    CanonicalHessianSecondVariationAtZero K hK :=
  h_second.canonical_secondVariation

/-- Phase-E cubic remainder theorem, conditional on the named Taylor input. -/
theorem reggeActionRemainder_cubic_bound
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_flat : FlatConfiguration K hK)
    (h_cubic : ReggeActionCubicRemainderInput K hK h_flat) :
    LocalCubicRemainderBound K hK :=
  h_cubic.cubic_bound

theorem hessianQuadratic_along_line_hasSecondDerivAt_zero
    (K : Triangulation3D) (H : Fin K.nV → Fin K.nV → ℝ)
    (ξ : VertexPotential K) :
    HasSecondDerivAt
      (fun t : ℝ => (1 / 2) * hessianQuadratic H (linePotential K ξ t))
      (hessianQuadratic H ξ) 0 := by
  unfold HasSecondDerivAt
  have hquad :
      (fun t : ℝ => (1 / 2) * hessianQuadratic H (linePotential K ξ t)) =
        fun t : ℝ => (hessianQuadratic H ξ / 2) * t ^ 2 := by
    funext t
    rw [hessianQuadratic_linePotential]
    ring
  rw [hquad]
  have hderiv :
      deriv (fun t : ℝ => (hessianQuadratic H ξ / 2) * t ^ 2) =
        fun t : ℝ => hessianQuadratic H ξ * t := by
    ext t
    have h :=
      ((hasDerivAt_id t).pow 2).const_mul (hessianQuadratic H ξ / 2)
    have h' : HasDerivAt
        (fun t : ℝ => (hessianQuadratic H ξ / 2) * t ^ 2)
        (hessianQuadratic H ξ * t) t := by
      simpa [id, two_mul, mul_comm, mul_left_comm, mul_assoc] using h
    exact h'.deriv
  rw [hderiv]
  simpa using (hasDerivAt_id 0).const_mul (hessianQuadratic H ξ)

What this page does not claim

The nonlinear second-variation calculation itself is not materialized; the analytic facts live in named input structures. The module does not prove that the flat configuration is a local minimum of the action. The cubic bound is not shown to hold for all displacements, only for small ones.

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