Geometry Regge Action First Variation Local Deficit Angle Contribution Has Deriv

The local deficit derivative

In the geometry of triangulated spaces, the Regge action is a discrete version of the Einstein-Hilbert action from general relativity. It is built from the deficit angle, the amount by which the angles around an edge fall short of a full circle, which measures curvature concentrated along that edge. The declaration deficitAngle_hasDerivAt_from_localAngles is a machine-checked theorem about how this deficit angle changes when the vertices of the triangulation move.

The theorem states a precise chain rule. Consider a one-parameter family of triangulations obtained by moving each vertex along a straight line in a chosen direction. The theorem says that the derivative of the deficit angle around a given edge, evaluated at the starting configuration, equals the sum over all tetrahedra that contain that edge of the derivative of the dihedral angle at that edge within each tetrahedron. In symbols, if t is the parameter, the derivative of the deficit angle is the negative sum of the derivatives of the local dihedral angles. This is the local, analytic version of the geometric fact that the total curvature around an edge is the sum of the contributions from the tetrahedra that meet there.

The proof is a direct application of the chain rule to the definition of the deficit angle as a sum of dihedral angles. The theorem assumes a package of local dihedral angle derivatives, which is a structure that supplies the derivative of each dihedral angle along the same line. It does not itself prove that such derivatives exist; that is a separate input. The theorem is a statement about the derivative of the deficit angle given those inputs, and it is valid for any triangulation and any direction of motion.

The theorem is one step in a larger project: showing that the first variation of the full Regge action vanishes at a flat configuration. That target is recorded as a structure ReggeActionFirstVariationInput, which requires the vanishing of the derivative of the action. The local deficit derivative theorem provides the analytic foundation for that calculation, but it does not by itself establish the vanishing. The full result also needs the Schläfli cancellation identity, which is a separate theorem in the library.

theorem deficitAngle_hasDerivAt_from_localAngles
    (K : Triangulation3D) (A : LocalDihedralDirectionalDerivativePackage K)
    (η : VertexPotential K) (e : Fin K.nE) :
    HasDerivAt
      (fun t : ℝ => deficitAngle K (linePotential K η t) e)
      (deficitDirectionalDerivFromLocalAngles K A η e) 0 := by
  unfold deficitAngle deficitDirectionalDerivFromLocalAngles
  have hsum : HasDerivAt
      (∑ τ : Fin K.nT,
        fun t : ℝ => localDeficitAngleContribution K (linePotential K η t) e τ)
      (∑ τ : Fin K.nT,
        match K.edgeInTet e τ with
        | none => 0
        | some f => A.angleDeriv η τ f) 0 := by
    have hsum' :=
      HasDerivAt.sum
        (u := Finset.univ)
        (A := fun τ t => localDeficitAngleContribution K (linePotential K η t) e τ)
        (A' := fun τ =>
          match K.edgeInTet e τ with
          | none => 0
          | some f => A.angleDeriv η τ f)
        (x := 0)
        (fun τ _ => localDeficitAngleContribution_hasDerivAt_from_localAngles K A η e τ)
    simpa using hsum'
  have hconst : HasDerivAt (fun _t : ℝ => 2 * Real.pi) 0 0 :=
    hasDerivAt_const 0 (2 * Real.pi)
  have hsub := hconst.sub hsum
  convert hsub using 1
  · ext t
    simp [Pi.sub_apply, Finset.sum_apply]
  · ring

theorem deficitAngle_hasDerivAt_from_localAngles
    (K : Triangulation3D) (A : LocalDihedralDirectionalDerivativePackage K)
    (η : VertexPotential K) (e : Fin K.nE) :
    HasDerivAt
      (fun t : ℝ => deficitAngle K (linePotential K η t) e)
      (deficitDirectionalDerivFromLocalAngles K A η e) 0 := by
  unfold deficitAngle deficitDirectionalDerivFromLocalAngles
  have hsum : HasDerivAt
      (∑ τ : Fin K.nT,
        fun t : ℝ => localDeficitAngleContribution K (linePotential K η t) e τ)
      (∑ τ : Fin K.nT,
        match K.edgeInTet e τ with
        | none => 0
        | some f => A.angleDeriv η τ f) 0 := by
    have hsum' :=
      HasDerivAt.sum
        (u := Finset.univ)
        (A := fun τ t => localDeficitAngleContribution K (linePotential K η t) e τ)
        (A' := fun τ =>
          match K.edgeInTet e τ with
          | none => 0
          | some f => A.angleDeriv η τ f)
        (x := 0)
        (fun τ _ => localDeficitAngleContribution_hasDerivAt_from_localAngles K A η e τ)
    simpa using hsum'
  have hconst : HasDerivAt (fun _t : ℝ => 2 * Real.pi) 0 0 :=
    hasDerivAt_const 0 (2 * Real.pi)
  have hsub := hconst.sub hsum
  convert hsub using 1
  · ext t
    simp [Pi.sub_apply, Finset.sum_apply]
  · ring

What this page does not claim

The theorem does not prove the existence of the derivatives of the dihedral angles; it assumes them as an input package. The theorem does not establish the vanishing of the first variation of the Regge action; that is a separate target requiring additional input. The theorem does not apply to degenerate tetrahedra where the dihedral angles are not defined.

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