Geometry Regge Action Smoothness Hinge Measure Under Conformal Cont Diff At Zero

The smooth flat point

Regge calculus is a discrete approach to general relativity where spacetime is approximated by a triangulated network, and the curvature is concentrated along shared edges, or hinges. The Regge action is the sum over these hinges of the deficit angle, the amount by which the surrounding tetrahedra fail to close flat. A central question is whether this action behaves smoothly as the geometry approaches a flat, zero-curvature state, or whether it develops a singularity there. The declaration hingeMeasureUnderConformal_contDiffAt_zero addresses a specific part of that question: it proves that the contribution of any single hinge to the action is infinitely differentiable with respect to a conformal rescaling of the edge lengths, precisely at the point where the geometry is flat.

To understand what this means, consider a conformal transformation as a smooth, pointwise stretching of the metric. In the discrete setting, this translates into multiplying the squared length of each edge by a positive factor derived from a potential at its vertices. The theorem states that as this potential varies, the hinge measure, the geometric quantity that enters the action, varies smoothly at the zero potential, which corresponds to the flat configuration. This is not a statement about the entire action at once; it is a local statement about one hinge at a time. The proof relies on the fact that the relevant denominators, derived from the Cayley-Menger determinant, are strictly positive for a nondegenerate tetrahedron, and that the arccosine arguments stay away from the endpoints that would make the angle ill-defined.

In the framework of Recognition Science, this smoothness result is a necessary ingredient for a larger goal: showing that the full nonlinear Regge action is well-behaved at flatness. The framework's library records the analytic requirements as a named configuration, LocalAnalyticFlatChart, a structure that packages the conditions that each tetrahedron is nondegenerate and that the arccosine arguments stay away from ±1. The theorem hingeMeasureUnderConformal_contDiffAt_zero is proved for any such chart, and it feeds into the proof that the entire action is smooth at the flat potential, a result stated as reggeAction_contDiff_at_zero. This is a technical but essential step: without smoothness, the action could not be used to define a well-behaved variational principle or a perturbative expansion around flat space.

The declaration does not claim that the action is smooth everywhere, nor that the flat configuration is unique. It only establishes smoothness at a single point, the zero potential, under the explicit condition that the geometry is locally nondegenerate and the arccosine arguments are safe. It also does not claim that global flatness follows from local smoothness; the framework explicitly notes that global zero-deficit flatness is an assembled-triangulation condition that does not follow from local nondegeneracy. The theorem is a local, analytic fact about a single hinge, not a global statement about the geometry.

theorem hingeMeasureUnderConformal_contDiffAt_zero
    (K : Triangulation3D) (hK : IncidenceConsistent K) (e : Fin K.nE) (n : ℕ∞) :
    ContDiffAt ℝ n (fun ξ : VertexPotential K =>
      hingeMeasureUnderConformal K hK ξ e) (zeroPotential K) :=
  (hingeMeasureUnderConformal_contDiff K hK e n).contDiffAt

/-- 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

/-- Local analytic chart data supplied by Euclidean realizations of every
tetrahedron in the triangulation.  This is the local ingredient behind strict
arccos endpoint avoidance. -/
structure LocalAnalyticFlatChart (K : Triangulation3D) where
  realizedTet : ∀ _τ : Fin K.nT, RealizedNonDegenerateTet
  realizes_tet : ∀ τ : Fin K.nT, (realizedTet τ).tet = K.tet τ

What this page does not claim

The action is smooth at all configurations, only at the flat point under the stated nondegeneracy conditions. Global flatness of the entire triangulation follows from the local smoothness of each hinge. The result provides a unique or preferred conformal chart; it only requires that one exists.

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: