Geometry Regge Action Smoothness Dihedral Cos3 Sq Continuous At Of Den Ne Zero

A smoothness condition

The Regge action is a way of writing gravity on a triangulated space, where the smooth fabric of spacetime is replaced by flat tetrahedra glued together along their faces. Its building blocks are dihedral angles, the angles between two faces of a tetrahedron. In the framework's machine-checked library of formal theorems, the quantity dihedralCos3Sq is a squared cosine derived from the Cayley-Menger matrix, a matrix whose entries encode the squared edge lengths of a tetrahedron.

The theorem dihedralCos3Sq_continuousAt_of_den_ne_zero proves that this squared cosine is a continuous function of the six squared edge lengths at any point where a related denominator, dihedralDenom3, is not zero. Continuity here means that a small change in the edge lengths produces a small change in the squared cosine. The proof works by expressing the squared cosine as a ratio of two continuous functions and then applying the standard fact that a ratio is continuous where the denominator is nonzero.

This lemma is a local analytic input for the full nonlinear Regge action. It is used to show that the action is smooth at a flat potential, a configuration where all deficit angles, the angles measuring curvature around an edge, are zero. The theorem itself does not claim that the denominator is always nonzero; that is a separate condition, guaranteed for nondegenerate tetrahedra. It also does not claim that the Regge action is smooth everywhere, only at specific configurations where the required hypotheses hold.

theorem dihedralCos3Sq_continuousAt_of_den_ne_zero
    (a : CayleyMengerPolynomial.SqEdges) (f : Fin 6)
    (hden : dihedralDenom3 a f ≠ 0) :
    ContinuousAt (fun x : CayleyMengerPolynomial.SqEdges => dihedralCos3Sq x f) a := by
  unfold dihedralCos3Sq
  exact (CayleyMengerMatrix.cmCofactor3_contDiff 0
      (DihedralCayleyMenger.oppositeCMVertices f).1
      (DihedralCayleyMenger.oppositeCMVertices f).2).continuous.continuousAt.div
    (dihedralDenom3_continuousAt a f) hden

theorem dihedralCos3Sq_continuousAt_of_den_ne_zero
    (a : CayleyMengerPolynomial.SqEdges) (f : Fin 6)
    (hden : dihedralDenom3 a f ≠ 0) :
    ContinuousAt (fun x : CayleyMengerPolynomial.SqEdges => dihedralCos3Sq x f) a := by
  unfold dihedralCos3Sq
  exact (CayleyMengerMatrix.cmCofactor3_contDiff 0
      (DihedralCayleyMenger.oppositeCMVertices f).1
      (DihedralCayleyMenger.oppositeCMVertices f).2).continuous.continuousAt.div
    (dihedralDenom3_continuousAt a f) hden

What this page does not claim

The denominator dihedralDenom3 is always nonzero. The Regge action is smooth everywhere on the space of all edge lengths. This lemma establishes the physical correctness of the Regge action as a theory of gravity.

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: