Geometry Regge Action First Variation Directional First Variation Formula Of Def

The first variation formula

Regge calculus is a discrete approach to general relativity in which spacetime is approximated by a triangulated manifold, a network of flat tetrahedra glued together along their faces. The Regge action is a sum over the edges, or hinges, of the product of an edge length and a deficit angle, which measures how much the surrounding tetrahedra fail to lie flat around that edge. The central tool for studying this action is its first variation, the derivative of the action with respect to small changes in the edge lengths. A critical point of the action, where this derivative vanishes, corresponds to a solution of the discrete Einstein equations. In the continuum, the vacuum Einstein equations are exactly the statement that the first variation of the Einstein-Hilbert action is zero.

The theorem directionalFirstVariationFormula_of_deficitPackage, proved in the framework's machine-checked library of formal theorems, establishes a precise formula for this first variation in a specific setting. It states that for a triangulated three-dimensional manifold with a consistent incidence structure, if the deficit angles and their directional derivatives are packaged in a certain way, then the directional first variation of the Regge action at the flat potential is given by that package. The flat potential is the configuration where all edge lengths are equal, and the directional derivative is taken along a line in the space of vertex potentials, which are functions assigning a real number to each vertex. The theorem is a formal statement of the geometric proof that the first variation vanishes at a flat configuration, a result that follows from the cancellation of local contributions, a discrete analogue of the Schläfli identity.

The theorem does not claim that the Regge action is minimized at the flat configuration, only that its first variation is zero there, making it a critical point. It also does not claim that this critical point is unique or that the second variation, which determines stability, has any particular sign. The theorem is a statement about the first variation only, and it requires the input of a package that provides the directional derivatives of the deficit angles. The theorem itself does not construct this package; it shows that if such a package exists, then the first variation formula follows. The proof of the existence of this package, and the full calculation of the second variation, are separate matters that the theorem does not address.

theorem directionalFirstVariationFormula_of_deficitPackage
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (D : DeficitAngleDirectionalDerivativePackage K hK) :
    ReggeActionDirectionalFirstVariationFormula K hK where
  directional_formula := by
    intro η
    unfold reggeAction
    have hedge :
        ∀ e : Fin K.nE,
          HasDerivAt
            (fun t : ℝ =>
              hingeMeasureUnderConformal K hK (linePotential K η t) e *
                deficitAngle K (linePotential K η t) e)
            (hingeMeasureDirectionalDeriv K hK η e *
                deficitAngle K (zeroPotential K) e +
              hingeMeasureUnderConformal K hK (zeroPotential K) e *
                D.deficitDeriv η e) 0 := by
      intro e
      have hL := hingeMeasureUnderConformal_hasDerivAt_line_zero K hK η e
      have hδ := D.deficit_hasDerivAt η e
      have hprod := hL.mul hδ
      simpa [linePotential_zero K η, mul_comm, mul_left_comm, mul_assoc] using hprod
    have hsum : HasDerivAt
        (∑ e : Fin K.nE,
          fun t : ℝ =>
            hingeMeasureUnderConformal K hK (linePotential K η t) e *
              deficitAngle K (linePotential K η t) e)
        (∑ e : Fin K.nE,
          (hingeMeasureDirectionalDeriv K hK η e *
              deficitAngle K (zeroPotential K) e +
            hingeMeasureUnderConformal K hK (zeroPotential K) e *
              D.deficitDeriv η e)) 0 := by
      have hsum' :=
        HasDerivAt.sum
            (u := Finset.univ)
            (A := fun e t =>
              hingeMeasureUnderConformal K hK (linePotential K η t) e *
                deficitAngle K (linePotential K η t) e)
            (A' := fun e =>
              hingeMeasureDirectionalDeriv K hK η e *
                  deficitAngle K (zeroPotential K) e +
                hingeMeasureUnderConformal K hK (zeroPotential K) e *
                  D.deficitDeriv η e)
            (x := 0)
            (fun e _ => hedge e)
      simpa [Finset.sum_apply] using hsum'
    have htarget :
        (∑ e : Fin K.nE,
          (hingeMeasureDirectionalDeriv K hK η e *
              deficitAngle K (zeroPotential K) e +
            hingeMeasureUnderConformal K hK (zeroPotential K) e *
              D.deficitDeriv η e)) =
        ∑ e : Fin K.nE,
          hingeMeasureDirectionalDeriv K hK η e *
            deficitAngle K (zeroPotential K) e := by
      rw [Finset.sum_add_distrib, D.schlaefli_cancellation η]
      ring
    rw [htarget] at hsum
    convert hsum using 1
    ext t
    simp

What this page does not claim

The theorem does not prove that the flat configuration is a minimum of the Regge action. It does not establish the existence of the deficit angle derivative package; it only derives the formula from it. It does not address the second variation or the stability of the critical point.

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: