Geometry Regge Action First Variation Conformal Schlaefli Cancellation Of Length

The flat-space check

In discrete geometry, the Regge action is a way to measure the total curvature of a space built from flat tetrahedra. It sums, over every edge, the edge length times the deficit angle, which is the amount by which the angles around the edge fall short of a full circle. A central question is whether this action is stable: whether a small, smooth change in the shape of the tetrahedra leaves the action unchanged to first order. The classical answer, for smooth spaces, is that the Einstein equations are the condition for this stability. The discrete analogue is a target for the framework's library.

The declaration conformalSchlaefliCancellation_of_lengthChain_of_bookkeeping establishes a precise, machine-checked version of this stability for a special family of changes. The changes are conformal: they scale the length of every edge in a tetrahedron by a single factor, which may vary from vertex to vertex. The theorem shows that, at the flat configuration where every deficit angle is zero, the first derivative of the action along any such conformal change vanishes. The proof works by a local cancellation: within each tetrahedron, the contribution from the changing dihedral angles is exactly cancelled by the contribution from the changing edge lengths. This is the discrete analogue of the Schläfli identity, a classical formula for how the volume of a polytope changes when its dihedral angles change.

The declaration is a theorem in the framework's machine-checked library of formal theorems. It is not a derivation of the Einstein equations, and it does not show that the action is stable under all changes, only under conformal ones. It also does not show that the flat configuration is a minimum, only that it is a critical point. The theorem is a consistency check: the framework's model of discrete geometry reproduces a known and necessary property of the Regge action.

/-- Local Schläfli cancellation for the conformal length direction on a single
tetrahedron.  This is pure finite-sum algebra plus the already proved local
Schläfli identity. -/
theorem local_conformal_schlaefli_cancellation
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (η : VertexPotential K) (τ : Fin K.nT) :
    (∑ f : Fin 6,
      Real.sqrt ((K.tet τ).sqEdge f) *
        localAngleLengthChainDeriv K hK η τ f) = 0 := by
  unfold localAngleLengthChainDeriv
  calc
    (∑ f : Fin 6,
      Real.sqrt ((K.tet τ).sqEdge f) *
        (∑ k : Fin 6,
          ((triangulationSchlaefliData_of_incidence K hK).tetData τ).dihedralDeriv f k *
            localEdgeLengthDirectionalDeriv K η τ k))
        =
      ∑ k : Fin 6,
        localEdgeLengthDirectionalDeriv K η τ k *
          (∑ f : Fin 6,
            Real.sqrt ((K.tet τ).sqEdge f) *
              ((triangulationSchlaefliData_of_incidence K hK).tetData τ).dihedralDeriv f k) := by
          simp_rw [Finset.mul_sum]
          rw [Finset.sum_comm]
          refine Finset.sum_congr rfl ?_
          intro k _
          refine Finset.sum_congr rfl ?_
          intro f _
          ring
    _ = ∑ k : Fin 6, localEdgeLengthDirectionalDeriv K η τ k * 0 := by
          refine Finset.sum_congr rfl ?_
          intro k _
          rw [((triangulationSchlaefliData_of_incidence K hK).tetData τ).schlaefli k]
    _ = 0 := by simp

/-- Local Schläfli cancellation for the conformal length direction on a single
tetrahedron.  This is pure finite-sum algebra plus the already proved local
Schläfli identity. -/
theorem local_conformal_schlaefli_cancellation
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (η : VertexPotential K) (τ : Fin K.nT) :
    (∑ f : Fin 6,
      Real.sqrt ((K.tet τ).sqEdge f) *
        localAngleLengthChainDeriv K hK η τ f) = 0 := by
  unfold localAngleLengthChainDeriv
  calc
    (∑ f : Fin 6,
      Real.sqrt ((K.tet τ).sqEdge f) *
        (∑ k : Fin 6,
          ((triangulationSchlaefliData_of_incidence K hK).tetData τ).dihedralDeriv f k *
            localEdgeLengthDirectionalDeriv K η τ k))
        =
      ∑ k : Fin 6,
        localEdgeLengthDirectionalDeriv K η τ k *
          (∑ f : Fin 6,
            Real.sqrt ((K.tet τ).sqEdge f) *
              ((triangulationSchlaefliData_of_incidence K hK).tetData τ).dihedralDeriv f k) := by
          simp_rw [Finset.mul_sum]
          rw [Finset.sum_comm]
          refine Finset.sum_congr rfl ?_
          intro k _
          refine Finset.sum_congr rfl ?_
          intro f _
          ring
    _ = ∑ k : Fin 6, localEdgeLengthDirectionalDeriv K η τ k * 0 := by
          refine Finset.sum_congr rfl ?_
          intro k _
          rw [((triangulationSchlaefliData_of_incidence K hK).tetData τ).schlaefli k]
    _ = 0 := by simp

What this page does not claim

The theorem does not derive the Einstein equations from the Regge action. The theorem does not prove stability under non-conformal changes to the edge lengths. The theorem does not show the flat configuration is a minimum of the action.

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: