deficitLineDeriv_differentiableAt_zero_of_flatConfiguration
plain-language theorem explainer
At a flat conformal configuration on an incidence-consistent 3D triangulation, the first derivative of each edge deficit angle along any vertex-potential line is differentiable at the origin. Second-variation and nonlinear Hessian arguments cite this to justify one more differentiation of the deficit at t=0. The proof is a one-line transfer: C^∞ of the deficit along the line plus a general fact that ContDiffAt top implies DifferentiableAt of the derivative.
Claim. Let $K$ be a 3D triangulation with consistent incidence, and suppose the zero vertex potential is flat. For every vertex potential $\xi$ and every global edge $e$, the map $t \mapsto \frac{d}{ds}\big|_{s=t} \delta_e(s\xi)$ is differentiable at $t=0$, where $\delta_e$ denotes the Regge deficit angle at $e$ under the conformal ansatz.
background
In the conformal Regge setting a vertex potential assigns a real scalar to each vertex; the line potential scales that assignment by a real parameter $t$. The deficit angle at a global edge $e$ is $2\pi$ minus the sum of local dihedral contributions from tetrahedra incident on $e$. Its ordinary derivative along the conformal line is the deficit-line derivative studied here.
The module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. Flat configuration means the zero potential realizes the geometric flatness condition used throughout the second-variation chain; incidence consistency ensures the triangulation gluing data are well-formed.
Upstream, infinite differentiability (ContDiffAt of order $\top$) of the deficit along any conformal line at $t=0$ is already proved under the same flat hypotheses. A general univariate calculus lemma then upgrades that smoothness to differentiability of the first derivative at the origin.
proof idea
Unfold the deficit-line derivative to the ordinary one-variable deriv of deficit angle along the line potential. Invoke the general lemma that ContDiffAt $\mathbb{R},\top$ of a real function at $0$ implies DifferentiableAt of its derivative at $0$. Feed that lemma the sibling theorem establishing ContDiffAt $\top$ for the deficit along the line at the flat point. No geometric expansion is recomputed; the argument is pure smoothness transfer.
why it matters
This is a local differentiability brick inside the nonlinear Hessian proof interface. Its sole recorded consumer packages hinge- and deficit-line second differentiability at zero into the target structure that feeds the chain-rule identification of the second directional derivative of the Regge action with the canonical incidence Hessian.
Once that identification is complete, the existing second-variation input structure follows and the discrete second-variation theory closes. In the Recognition Geometry stack this supports the claim that the linearized conformal Regge operator at flat space is a well-defined quadratic form on a 3D spatial triangulation (consistent with the forcing chain step that fixes $D=3$). The lemma only guarantees existence of the second derivative so the value comparison is well-posed; it does not evaluate the Hessian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.