Geometry Regge Action Second Variation Hessian Quadratic Along Line Has Second D

The directional second derivative

The declaration proves a basic fact about quadratic forms. A quadratic form is a function that takes a vector and returns a number, built from products of its components. The theorem considers a fixed quadratic form, a fixed direction vector, and the straight line obtained by scaling that vector by a real number t. It shows that the function which sends t to one half of the quadratic form evaluated at that scaled vector has a second derivative at t equals 0, and that this second derivative is exactly the quadratic form evaluated at the original direction vector.

In symbols, if H is the matrix of the quadratic form and ξ is the direction vector, then the theorem states that the second derivative at zero of the function t ↦ (1/2) H(tξ, tξ) is H(ξ, ξ). This is the standard calculus result for a quadratic function: the second derivative of (1/2) a t² is a. The theorem is a formal, machine-checked statement of this fact within the framework's library of formal theorems. It is a ledger, a discrete record of events, entry that confirms the consistency of the framework's definitions.

The theorem does not claim that the full, nonlinear Regge action, a discrete model of spacetime curvature, has this second derivative. That statement, called CanonicalHessianSecondVariationAtZero, is a separate target that depends on an unproven input structure. The proved theorem concerns only the quadratic part, the hessianQuadratic function, and not the actual action. It also does not establish any property of the action's remainder term or any cubic bound; those are separate targets with their own named inputs.

Within the framework, this theorem is a stepping stone. It is a fully proved fact about the quadratic approximation, which the framework uses to structure its analysis of the nonlinear action. The theorem's value is that it is unconditional: it holds for any triangulation and any direction vector, with no extra assumptions. This makes it a reliable foundation for the framework's geometric investigations, even though the larger claims about the full action remain open targets.

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 full nonlinear Regge action has this second derivative at zero. The canonical remainder term is zero or satisfies a cubic bound. The theorem holds for any function other than the specific quadratic form hessianQuadratic.

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: