Geometry Regge Action Smoothness

Smoothness at the flat configuration

In lattice gravity, the Regge action replaces smooth spacetime with a triangulated manifold, a collection of flat tetrahedra glued along their faces. Curvature is concentrated along the shared edges, or hinges, and measured by the deficit angle: the amount by which the angles around an edge fail to sum to 2π. The action is the sum over edges of the hinge length times the deficit angle. This construction is classical, going back to Tullio Regge in 1961.

The action is smooth when the deficit angle varies smoothly as the edge lengths change. A problem appears at the flat configuration, where all deficit angles are zero. The formula for the dihedral angle of a tetrahedron involves an arccosine, and that function has a derivative singularity when its argument approaches ±1. If an edge length perturbation drives the arccosine argument to an endpoint, the action loses differentiability. The framework's library records these analytic requirements as a named configuration rather than hiding them as axioms.

In Recognition Science, the library proves that the action is smooth at the flat potential, provided two conditions hold. First, the conformal edge chart must stay inside the nondegenerate tetrahedral cone, meaning no tetrahedron collapses to zero volume. Second, the arccosine arguments must stay away from ±1. Under those conditions, the theorem reggeAction_contDiff_at_zero establishes that the action is infinitely differentiable at the flat configuration. The proof assembles smoothness from the polynomial and strict interior facts already proved in the geometry stack.

The flat configuration itself is a global condition, not a local one. The theorem GlobalZeroDeficitAtFlat states that every edge must have zero deficit angle at the zero potential, which does not follow from local nondegeneracy of each tetrahedron. The structure FlatConfiguration packages the endpoint-free arccosine condition, the zero-deficit condition, and the smoothness condition into one object. From a local analytic chart and a global zero-deficit assumption, the library constructs a flat configuration, showing the three requirements are compatible.

What this establishes in plain language: the Regge action, despite its arccosine singularities, is well-behaved at the flat point when the triangulation is nondegenerate and the arccosine arguments stay interior. This smoothness is a prerequisite for any variational or perturbative treatment of the action in the framework. Without it, the second-order component theorem's exact quadratic truncation would have no analytic foundation for the full nonlinear action.

/-- Phase-A smoothness theorem for the nonlinear action, conditional on the
named flat analytic configuration. -/
theorem reggeAction_contDiff_at_zero
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_flat : FlatConfiguration K hK) :
    ContDiffAt ℝ (⊤ : ℕ∞) (reggeAction K hK) (zeroPotential K) :=
  h_flat.action_contDiff_at_zero

/-- Global zero-deficit flatness is an assembled-triangulation condition.  It
does not follow from local nondegeneracy of each tetrahedron. -/
def GlobalZeroDeficitAtFlat (K : Triangulation3D) : Prop :=
  ∀ e : Fin K.nE, deficitAngle K (zeroPotential K) e = 0

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 module does not prove that the Regge action is smooth everywhere, only at the flat configuration under stated conditions. The module does not derive the Regge action from first principles; it takes the classical action as given and analyzes its analytic properties.

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: