Geometry Regge Action Nonlinear Hessian Proof Canonical Remainder Line Different

The differentiability bridge

The Regge action is a discrete model of gravity built from a triangulated space, where the curvature is concentrated along the hinges (edges in three dimensions) and measured by the deficit angle, the amount by which the surrounding tetrahedra fail to close flat. The action is a sum over hinges of the hinge length times the deficit angle. For the framework's program, the key question is whether this nonlinear action has a well-defined second derivative at the flat configuration, the point where all deficit angles are zero. That second derivative, if it exists, should match the canonical quadratic form built from the incidence structure of the triangulation.

The declaration canonicalRemainderLineDifferentiabilityNearZero_of_actionLineDifferentiabilityNearZero is a theorem in the machine-checked library of formal theorems. It states: if the action is differentiable at every point along every straight line through the flat configuration, then the remainder term, defined as the action minus its canonical quadratic approximation, is also differentiable at every point along every such line. The remainder is the object that isolates the difference between the full nonlinear action and its quadratic model. The theorem is a bridge: it transfers a differentiability property from the full action to the remainder, which is the term that must vanish to second order for the canonical Hessian to be the true second variation.

This is a local statement about the neighborhood of the flat configuration. The theorem assumes differentiability of the action along lines near zero, not just at zero. It does not claim that the remainder is zero, nor that the canonical Hessian equals the second derivative of the action. It only establishes that the remainder is differentiable, which is a necessary precondition for asking whether its second derivative is zero. The theorem is one step in a larger proof interface that isolates the remaining hard calculation: showing that the second directional derivative of the remainder at the flat configuration is zero.

In the framework, this theorem is part of the proof that the nonlinear Regge action reduces to the canonical incidence Hessian, the discrete analog of the Einstein-Hilbert action's second variation. The differentiability bridge is what allows the framework to separate the quadratic part, which is understood, from the nonlinear remainder, which must be shown to vanish to second order. The theorem does not prove that vanishing; it proves the differentiability that makes the question well-posed.

/-- Concrete differentiability condition sufficient for the derivative identity.
This is the target the smoothness chain should supply for the action line; the
quadratic line is elementary. -/
def CanonicalRemainderLineDifferentiabilityTarget
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∀ (ξ : VertexPotential K) (t : ℝ),
    DifferentiableAt ℝ (actionAlongLine K hK ξ) t ∧
      DifferentiableAt ℝ (canonicalQuadraticAlongLine K hK ξ) t

What this page does not claim

The theorem does not claim that the remainder is zero or that its second derivative vanishes. The theorem does not claim that the action is differentiable, only that its differentiability implies the remainder's differentiability. The theorem does not establish the full nonlinear Regge Hessian result, which remains an open target.

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: