Encyclopedia Geometry Geometry Regge Action First Variation Directional Critical Of First Variation Fo

ARTICLE 4 claims 3 theorems 1 model

Geometry Regge Action First Variation Directional Critical Of First Variation Fo

In Regge calculus, a discrete model of spacetime, the flat geometry is a stationary point of the action: the first tiny change in any direction leaves the total action unchanged.

Verify this page

The flat-space critical point

In Regge calculus, spacetime is approximated by a grid of flat tetrahedra joined along their triangular faces. The Regge action is a number assigned to such a grid, built from the lengths of its edges and the angles where tetrahedra meet. A central question is which grid geometries are physically allowed, and the answer in variational calculus is that a geometry is allowed when it is a critical point of the action: a small change in the geometry produces no first-order change in the action. The declaration directionalCritical_of_firstVariationFormula_of_zeroDeficit records a precise statement about this condition at one particular geometry, the flat one.

The flat geometry is the one where all tetrahedra lie in ordinary Euclidean space with no curvature concentrated along their edges. The declaration states that this flat geometry is a directional critical point of the Regge action. Directional means the statement is checked along every possible straight-line path in the space of geometries, not just along a few special directions. The proof rests on two classical facts. The first is Schläfli's identity, a relation between how a tetrahedron's volume changes and how its dihedral angles change. The second is that in a flat configuration, the total deficit angle around every edge is zero, which is the discrete analogue of saying space is not curved there.

The declaration itself is a definition, not a theorem. It packages the condition that the derivative of the Regge action at the flat potential is zero in every direction. The library also contains a theorem, directionalFirstVariationFormula_of_deficitPackage, which derives this condition from the deficit-angle derivative package, and another theorem that converts the directional statement into the full statement that the derivative is zero. The input structure ReggeActionFirstVariationInput records the assumption that this first variation vanishes, and a separate theorem, reggeAction_firstVariation_zero, uses that assumption to conclude the derivative is zero.

What the declaration does not claim is that the flat geometry is a minimum of the action, only that it is a critical point. It does not claim that the flat geometry is the only critical point, nor that the second variation, which would determine stability, is positive. It also does not claim that the full derivative calculation is complete in the library; the docstring notes that the full derivative calculation is a target, with the current module recording the exact analytic statement and the named input needed until the calculation is expanded from the closed-form local Schläfli identities.

MODEL ReggeActionDirectionalCriticalAtZero · IndisputableMonolith/Geometry/ReggeActionFirstVariation.lean
ReggeActionDirectionalCriticalAtZero · IndisputableMonolith/Geometry/ReggeActionFirstVariation.lean:312 
/-- Directional form of criticality, useful while deriving the first
variation by differentiating along lines. -/
def ReggeActionDirectionalCriticalAtZero
    (K : Triangulation3D) (hK : IncidenceConsistent K) : Prop :=
  ∀ η : VertexPotential K,
    (fderiv ℝ (reggeAction K hK) (zeroPotential K)) η = 0
THEOREM local_conformal_schlaefli_cancellation · directionalFirstVariationFormula_of_deficitPackage · IndisputableMonolith/Geometry/ReggeActionFirstVariation.lean
local_conformal_schlaefli_cancellation · IndisputableMonolith/Geometry/ReggeActionFirstVariation.lean:456 
/-- 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
directionalFirstVariationFormula_of_deficitPackage · IndisputableMonolith/Geometry/ReggeActionFirstVariation.lean:888 
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
THEOREM directionalFirstVariationFormula_of_deficitPackage · IndisputableMonolith/Geometry/ReggeActionFirstVariation.lean
directionalFirstVariationFormula_of_deficitPackage · IndisputableMonolith/Geometry/ReggeActionFirstVariation.lean:888 
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
THEOREM reggeActionCriticalAtZero_of_directional · IndisputableMonolith/Geometry/ReggeActionFirstVariation.lean
reggeActionCriticalAtZero_of_directional · IndisputableMonolith/Geometry/ReggeActionFirstVariation.lean:319 
theorem reggeActionCriticalAtZero_of_directional
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hdir : ReggeActionDirectionalCriticalAtZero K hK) :
    ReggeActionCriticalAtZero K hK := by
  unfold ReggeActionCriticalAtZero
  ext η
  exact hdir η

What this page does not claim

The flat geometry is a minimum of the action, only a critical point. The flat geometry is the only critical point of the Regge action. The full derivative calculation is complete in the machine-checked library; it is a stated target.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND