Geometry Regge Action Smoothness Dihedral Cos3 Sq Conformal Cont Diff At Zero

Smoothness at the flat configuration

In the study of discrete gravity, the Regge action is a way to define the total gravitational energy of a triangulated space, a space built from flat tetrahedra joined along their faces. The action is a sum over the tetrahedra's edges, with each term involving the edge length and the deficit angle, the angle by which the flat tetrahedra fail to close up around that edge. For the action to be physically useful, it must be a smooth function of the geometry, meaning small changes in the positions of the vertices produce small, predictable changes in the action.

The declaration dihedralCos3Sq_conformal_contDiffAt_zero is a theorem in the framework's machine-checked library of formal theorems. It proves that a particular piece of the action, the square of the cosine of a dihedral angle (the angle between two faces of a tetrahedron) under a specific conformal (angle-preserving) change of the vertex positions, is infinitely differentiable at the point where the geometry is completely flat. This is a local statement: it concerns behavior near the flat configuration, not for all possible geometries.

This smoothness result is not automatic. The formula for the dihedral angle involves an arccosine, which has a derivative that blows up when its argument approaches 1 or -1. The theorem's proof relies on showing that, for a non-degenerate tetrahedron (one with non-zero volume), this problematic endpoint is never reached, and that the denominator in the formula never vanishes. The theorem is a key ingredient in proving that the full Regge action itself is smooth at the flat configuration, a property needed for the action to have a well-defined derivative and for perturbation theory to be applicable.

The theorem does not claim that the Regge action is smooth everywhere, nor does it say that the flat configuration is a minimum of the action. It only establishes smoothness at that single point, under the condition that the triangulation is non-degenerate. It also does not prove that the action is analytic, only that it is infinitely differentiable. The result is a technical foundation, not a physical law in itself.

theorem dihedralCos3Sq_conformal_contDiffAt_zero
    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) (n : ℕ∞) :
    ContDiffAt ℝ n (fun ξ : VertexPotential K =>
      dihedralCos3Sq (conformalTetSqEdges K ξ τ) f) (zeroPotential K) := by
  unfold dihedralCos3Sq
  let p := (DihedralCayleyMenger.oppositeCMVertices f).1
  let q := (DihedralCayleyMenger.oppositeCMVertices f).2
  have hnum := cmCofactor3_conformal_contDiffAt_zero K τ p q n
  have hden := dihedralDenom3_conformal_contDiffAt_zero K τ f n
  have hden_ne :
      dihedralDenom3 (conformalTetSqEdges K (zeroPotential K) τ) f ≠ 0 := by
    simpa [conformalTetSqEdges_zero K τ] using local_dihedralDenom3_ne_zero K τ f
  simpa [p, q] using hnum.div hden hden_ne

theorem local_dihedralDenom3_ne_zero
    (K : Triangulation3D) (τ : Fin K.nT) (f : Fin 6) :
    dihedralDenom3 ((K.tet τ).sqEdge) f ≠ 0 := by
  rw [dihedralDenom3_eq_poly]
  exact local_dihedralDenom3Poly_ne_zero K τ f

What this page does not claim

The theorem does not prove the Regge action is smooth everywhere, only at the flat configuration. The theorem does not claim the flat configuration is a minimum of the action. The theorem does not establish that the action is analytic, only that it is infinitely differentiable.

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