Geometry Regge Action Smoothness Regge Action Cont Diff At Zero Of Local Chart

Smoothness at the flat configuration

The Regge action is a way to do general relativity without smooth manifolds: it replaces spacetime with a triangulated network of flat tetrahedra, and measures curvature by how much the angles around each edge fail to sum to a full circle. That failure is called the deficit angle, a discrete record of how much geometry bends at a hinge. In the Recognition Science framework's machine-checked library of formal theorems, a declaration named reggeAction_contDiffAt_zero_of_localChart establishes a precise smoothness property of this action.

The theorem states that, given a triangulation with consistent incidence data and a local analytic flat chart, the Regge action is infinitely differentiable at the zero potential, the point where all vertex potentials vanish and the geometry is flat. In plain terms, the action function has no kinks, cusps, or jumps as the geometry passes through the flat configuration. This is a local statement about a single point in the space of possible geometries, not a global statement about the entire space.

The proof rests on a chain of supporting facts. Each tetrahedron in the triangulation must be nondegenerate, meaning its volume is not zero and its dihedral angles are well defined. The arguments of the arccosine functions that compute those angles must stay away from the endpoints ±1, where the derivative would blow up. Under these conditions, the library proves that the squared edge lengths, the Cayley-Menger cofactors, the dihedral angle cosines, and the hinge measures all vary smoothly with the potential, and so does the full action.

In Recognition Science, this smoothness result is a technical input, not a physical law. It does not claim that the flat configuration is a minimum or a maximum of the action, nor that the action is smooth everywhere. It does not assert that the flat geometry is dynamically preferred. The theorem only guarantees that the action is well behaved enough at that one point for calculus to work, which is a prerequisite for studying small fluctuations around flat spacetime.

theorem reggeAction_contDiffAt_zero_of_localChart
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (hChart : LocalAnalyticFlatChart K) :
    ContDiffAt ℝ (⊤ : ℕ∞) (reggeAction K hK) (zeroPotential K) :=
  reggeAction_contDiffAt_zero_of_endpoint_free K hK
    hChart.local_arccos_endpoint_free

What this page does not claim

The theorem does not claim the flat configuration is a minimum or maximum of the action. It does not claim the action is smooth everywhere, only at the zero potential under specific conditions. It does not assert that the flat geometry is dynamically preferred or physically realized.

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: