Geometry Regge Action Smoothness Regge Action Cont Diff At Zero Of Endpoint Free

Smoothness at the flat point

In the geometry of a triangulated space, the Regge action (a discrete sum over edges that measures curvature as an angle deficit) is built from arccos functions, which are smooth except where their argument is exactly plus or minus one. The declaration reggeAction_contDiffAt_zero_of_endpoint_free is a theorem in the machine-checked library of formal theorems. It proves that, for a three-dimensional triangulation with consistent incidence, if every dihedral angle's cosine-squared stays away from the endpoints 1 and -1, then the entire Regge action is infinitely differentiable at the zero potential, the configuration where all edge lengths are one and the deficit angles vanish.

The theorem is the final link in a chain that assembles the action from local pieces. Each tetrahedron's squared edge lengths, produced by a conformal map from vertex potentials, are smooth functions. The Cayley-Menger cofactors and denominators that enter the dihedral angle formula are smooth where the denominator is nonzero, and the endpoint-free hypothesis guarantees exactly that. Summing the local deficit-angle contributions over edges and tetrahedra preserves smoothness. The result is a ContDiffAt statement at the flat potential, meaning the action has derivatives of every order there, not merely a first derivative.

The theorem does not claim that the action is smooth everywhere, only at the flat point. It does not assert that a flat configuration exists; that is a separate condition, FlatConfiguration, which bundles the endpoint-free hypothesis with the vanishing of all deficit angles. The endpoint-free hypothesis is local to each tetrahedron, while global zero-deficit flatness is an assembled-triangulation condition that does not follow from local nondegeneracy. The theorem also does not prove that the action is analytic, only that it is infinitely differentiable.

theorem reggeAction_contDiffAt_zero_of_endpoint_free
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hEndpoint :
      ∀ τ : Fin K.nT, ∀ f : Fin 6,
        dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ -1 ∧
          dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ 1) :
    ContDiffAt ℝ (⊤ : ℕ∞) (reggeAction K hK) (zeroPotential K) := by
  unfold reggeAction
  simpa using
    (ContDiffAt.sum
      (s := Finset.univ)
      (f := fun e ξ =>
        hingeMeasureUnderConformal K hK ξ e * deficitAngle K ξ e)
      (x := zeroPotential K)
      (fun e _ =>
        (hingeMeasureUnderConformal_contDiffAt_zero K hK e (⊤ : ℕ∞)).mul
          (deficitAngle_contDiffAt_zero K e ⊤ hEndpoint)))

What this page does not claim

The theorem does not claim the Regge action is smooth everywhere, only at the flat potential. It does not assert that a flat configuration exists; that is a separate condition. It does not prove analyticity, only infinite differentiability.

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: