deficitAngle_contDiffAt_zero
plain-language theorem explainer
At the flat (zero) vertex potential, the Regge deficit angle on any global edge is C^n in the conformal potentials, provided every tetrahedral dihedral cosine stays strictly inside (-1,1). Discrete-gravity and Regge-calculus workers cite this to justify differentiating the nonlinear action at flat space. The proof unfolds the deficit as 2π minus a finite sum and subtracts the already-proved local contribution smoothness.
Claim. Let $K$ be a 3D triangulation and $e$ a global edge. Suppose that for every tetrahedron $\tau$ and every local edge $f$, the squared dihedral cosine built from Cayley–Menger cofactors satisfies $\cos^2\theta_{\tau,f}\neq\pm 1$. Then for every $n\in\mathbb{N}\cup\{\infty\}$, the map sending a vertex potential $\xi$ to the Regge deficit angle of $e$ is $C^n$ at the zero potential.
background
This module supplies analytic hypotheses for the full nonlinear Regge action: the conformal edge chart must remain in the nondegenerate tetrahedral cone, arccos arguments must avoid $\pm 1$, and the finite action must be smooth at the flat potential. Those requirements are packaged as named configuration facts rather than axioms.
The deficit angle at a global edge is $2\pi$ minus the sum, over all tetrahedra, of the local incidence contributions. Each local term is either zero (edge not in the tet) or the dihedral angle of the conformal image of that tet. Dihedral cosines are read from Cayley–Menger cofactors via dihedralCos3Sq.
Vertex potentials parameterize a conformal ansatz on edge lengths; the zero potential is the flat reference configuration. The local contribution smoothness theorem already gives $C^n$ for each summand at zero under the same endpoint-free hypothesis on dihedral cosines.
proof idea
Unfold the deficit angle definition: it is the constant $2\pi$ minus the sum over tetrahedra of the local incidence contributions. Apply ContDiffAt.sum over the finite universe of tetrahedra, feeding in localDeficitAngleContribution_contDiffAt_zero for each summand (with the endpoint hypothesis specialized to that tet). Conclude by subtracting that smooth sum from a constant via contDiffAt_const.sub.
why it matters
Smoothness of the deficit at flat space is the hinge-level input needed before the full Regge action can be differentiated. Downstream, reggeAction_contDiffAt_zero_of_endpoint_free lifts this edgewise fact to the global action, and deficitLine_contDiffAt_zero_of_flatConfiguration obtains $C^\infty$ smoothness of the deficit along conformal lines through a flat configuration.
In the Recognition geometry stack this sits under the nonlinear Hessian program for 3D Regge calculus: exact quadratic truncation is already closed, and these analytic lemmas open the door to the genuine nonlinear second variation at flat space. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete differential geometry supporting that later curvature analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.