Geometry Regge Action Nonlinear Hessian Proof Canonical Remainder Derivative Ide

The remainder's derivative identity

The declaration concerns the Regge action, a discrete model of gravity where spacetime is built from flat tetrahedra glued together. The action is a sum over the tetrahedra's edges, or hinges, of the edge length times a deficit angle, which measures how much the geometry fails to be flat around that edge. The framework's library, a machine-checked collection of formal theorems, is working toward showing that the second derivative of this action, at a flat configuration, equals a specific quadratic form known as the canonical incidence Hessian.

The theorem in question, canonicalRemainderDerivativeIdentity_of_lineDifferentiability, is a precise step in that calculation. It states that if the action and a related canonical quadratic term are differentiable along any line through the configuration space, then the derivative of the remainder term, the difference between the true action and the quadratic approximation, is zero at the origin. In plainer terms, it says that the error term in the quadratic approximation is 'flat' to first order at the flat configuration: it has no linear piece, only higher-order corrections. This is a standard and necessary condition for the quadratic form to be the correct second-order approximation.

The theorem does not prove that the remainder's second derivative is zero, nor does it establish the differentiability conditions it assumes. Those are separate targets within the same module. It also does not claim that the full nonlinear Regge action is quadratic, only that its second directional derivative at the flat potential matches the canonical Hessian. The result is a formal bridge: given the differentiability input, it derives the identity that the remaining hard calculation needs to close the proof.

theorem canonicalRemainderDerivativeIdentity_of_lineDifferentiability
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hDiff : CanonicalRemainderLineDifferentiabilityTarget K hK) :
    CanonicalRemainderDerivativeIdentityTarget K hK := by
  intro ξ
  funext t
  rw [canonicalRemainderAlongLine_eq_action_sub_quadratic K hK ξ]
  have hAction : DifferentiableAt ℝ (actionAlongLine K hK ξ) t := (hDiff ξ t).1
  have hQuad : DifferentiableAt ℝ (canonicalQuadraticAlongLine K hK ξ) t := (hDiff ξ t).2
  have hActionSubConst :
      DifferentiableAt ℝ
        (fun s : ℝ => actionAlongLine K hK ξ s -
          reggeAction K hK (zeroPotential K)) t :=
    hAction.sub (differentiableAt_const
      (c := reggeAction K hK (zeroPotential K)))
  have hSub := deriv_sub hActionSubConst hQuad
  calc
    deriv
        (fun s : ℝ =>
          actionAlongLine K hK ξ s - reggeAction K hK (zeroPotential K) -
            canonicalQuadraticAlongLine K hK ξ s) t
        = deriv
            (fun s : ℝ =>
              actionAlongLine K hK ξ s - reggeAction K hK (zeroPotential K)) t -
            deriv (canonicalQuadraticAlongLine K hK ξ) t := by
            simpa [sub_eq_add_neg] using hSub
    _ = deriv (actionAlongLine K hK ξ) t -
          deriv (canonicalQuadraticAlongLine K hK ξ) t := by
          rw [deriv_sub_const]

What this page does not claim

The theorem does not prove the differentiability assumptions it takes as input. It does not show the remainder's second derivative is zero, only its first derivative at the origin. It does not claim the full nonlinear Regge action is quadratic everywhere.

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: