localDeficitAngleContribution_contDiffAt_zero
plain-language theorem explainer
At the flat (zero) vertex potential, each tetrahedron's local contribution to the Regge deficit angle along a global edge is C^n-smooth for any extended order n, provided no dihedral cosine of that tet sits at ±1. Discrete-gravity and Regge-calculus workers cite this when assembling smoothness of the full nonlinear action. The proof is a two-branch case split on edge-tet incidence: constant zero off-incidence, otherwise the already-proved conformal dihedral-angle smoothness lemma.
Claim. Fix a 3D triangulation $K$, a global edge $e$, a tetrahedron $\tau$, and an extended differentiability order $n\in\mathbb{N}\cup\{\infty\}$. Assume that for every local edge slot $f$ of $\tau$, the squared dihedral cosine built from Cayley-Menger cofactors on the squared edge lengths of $\tau$ is neither $-1$ nor $1$. Then the map sending a vertex potential $\xi$ to the local incidence contribution of $(\tau,e)$ to the deficit angle 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 stay off $\pm 1$, and the finite action must be smooth at the flat potential. Those requirements are packaged as named configuration facts rather than axioms.
A local deficit-angle contribution is the incidence term for one global edge and one tetrahedron: if the edge belongs to the tet (via the incidence map edgeInTet), the contribution is the dihedral angle of that local edge after a conformal deformation driven by the vertex potential; otherwise it is zero. Dihedral cosines are read from Cayley-Menger cofactors on squared edge lengths (dihedralCos3Sq). The vertex potential is the discrete conformal degree of freedom on vertices; the zero potential is the flat reference configuration.
Upstream, smoothness of each conformal dihedral angle at zero is already available under the same endpoint (cosine $\neq\pm 1$) hypothesis. The present statement only lifts that fact through the incidence match that defines the local contribution.
proof idea
Unfold the local contribution. Case on the incidence option K.edgeInTet e τ.
- If the edge does not meet the tetrahedron, the contribution is the constant zero function of the potential; constant maps are $C^n$ at every point, hence at the zero potential.
- If incidence returns a local slot $f$, the contribution equals the conformal dihedral angle of that slot. Apply the upstream lemma that this angle map is $C^n$ at zero under the endpoint hypothesis specialized to $f$.
Both branches finish by simpa rewriting the match. No new analytic estimates appear here; the work is pure case dispatch onto prior smoothness.
why it matters
The full edge deficit angle is a finite sum of these local contributions over all tetrahedra. The immediate parent theorem deficitAngle_contDiffAt_zero therefore obtains global deficit smoothness at the flat potential by summing the present local statements under a uniform endpoint hypothesis on every tet.
In the Recognition geometry stack this is an analytic input to the nonlinear Regge action, not a forcing-chain landmark (T0-T8). The closed second-order component theorem already works with an exact quadratic truncation; the nonlinear theory needs precisely this $C^n$ control at the flat chart so that Hessian and higher variations are well-defined. The module frames these facts as configuration hypotheses rather than hidden axioms, keeping the analytic gap explicit for later discharge by interior/nondegeneracy lemmas already present in the geometry stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.