Geometry Regge Action Smoothness Local Deficit Angle Contribution Cont Diff At Z

Local smoothness at flatness

In Regge calculus, a discrete model of general relativity, space is built from flat tetrahedra glued along triangular faces. Curvature is not a field but a set of deficit angles: the angle by which the tetrahedra around an edge fail to close up flat. The framework's theorem localDeficitAngleContribution_contDiffAt_zero proves that, for any single tetrahedron's contribution to the deficit angle at a given edge, the contribution is a smooth function of the vertex potentials (the variables that set the tetrahedra's sizes) in a neighborhood of the flat configuration, where all deficit angles are zero.

Smoothness here means the contribution has derivatives of every order with respect to those potentials. The theorem holds for every tetrahedron and every edge, and for every order of differentiability. Its one explicit condition is that the cosine of the dihedral angle at each edge of the tetrahedron stays away from the endpoints ±1. That keeps the arccosine function, which recovers the angle from its cosine, well-behaved and differentiable. The proof chains together earlier results: the squared edge lengths vary smoothly under the conformal map, the Cayley-Menger cofactors that build the cosine are smooth, and the denominator in the cosine expression never vanishes on a nondegenerate tetrahedron.

The theorem is a local statement. It says nothing about the global condition that all deficit angles vanish simultaneously across the whole triangulation; that is a separate assembled condition, not a consequence of each tetrahedron being nondegenerate. It also does not claim that the full Regge action is smooth everywhere, only at the flat potential, and only under the endpoint condition. The framework packages these analytic requirements as a named configuration, FlatConfiguration, rather than hiding them as axioms, and the theorem is one of the supporting lemmas that feed the proof that the full action is smooth at flatness.

What this buys, in plain terms: the discrete geometry does not develop a singularity exactly at the flat state. That is the analytic foothold the framework needs to justify studying the action's behavior near flatness, for example when asking how small perturbations behave. The theorem is a regularity result, not a statement about the action's value or about the physics of the flat state itself.

theorem localDeficitAngleContribution_contDiffAt_zero
    (K : Triangulation3D) (e : Fin K.nE) (τ : Fin K.nT) (n : ℕ∞)
    (hEndpoint :
      ∀ f : Fin 6,
        dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ -1 ∧
          dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ 1) :
    ContDiffAt ℝ n (fun ξ : VertexPotential K =>
      localDeficitAngleContribution K ξ e τ) (zeroPotential K) := by
  unfold localDeficitAngleContribution
  cases h : K.edgeInTet e τ with
  | none =>
      simpa [h]
        using (contDiffAt_const :
          ContDiffAt ℝ n (fun _ξ : VertexPotential K => (0 : ℝ)) (zeroPotential K))
  | some f =>
      simpa [h] using tetDihedralAngleUnderConformal_contDiffAt_zero
        K τ f n (hEndpoint f)

theorem localDeficitAngleContribution_contDiffAt_zero
    (K : Triangulation3D) (e : Fin K.nE) (τ : Fin K.nT) (n : ℕ∞)
    (hEndpoint :
      ∀ f : Fin 6,
        dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ -1 ∧
          dihedralCos3Sq ((K.tet τ).sqEdge) f ≠ 1) :
    ContDiffAt ℝ n (fun ξ : VertexPotential K =>
      localDeficitAngleContribution K ξ e τ) (zeroPotential K) := by
  unfold localDeficitAngleContribution
  cases h : K.edgeInTet e τ with
  | none =>
      simpa [h]
        using (contDiffAt_const :
          ContDiffAt ℝ n (fun _ξ : VertexPotential K => (0 : ℝ)) (zeroPotential K))
  | some f =>
      simpa [h] using tetDihedralAngleUnderConformal_contDiffAt_zero
        K τ f n (hEndpoint f)

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

What this page does not claim

The theorem does not prove the full Regge action is smooth everywhere, only at the flat potential under the endpoint condition. The theorem does not establish that all deficit angles vanish simultaneously for the whole triangulation. The theorem does not make any statement about the value of the action or the physics of the flat state itself.

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: