deficitLine_contDiffAt_zero_of_flatConfiguration
plain-language theorem explainer
Along any straight line of vertex potentials through the flat background, the Regge deficit angle at a fixed edge is C^∞ at the origin. Anyone proving second-variation or Hessian identities for the nonlinear conformal Regge action cites this. The argument is ContDiffAt composition: the line map is smooth, and deficitAngle is smooth at the zero potential under the flat-configuration hypothesis.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat, let $\xi$ be a vertex potential on $K$, and let $e$ be a global edge. Then the real map $t \mapsto \delta_e\bigl(\xi_0 + t\xi\bigr)$, where $\delta_e$ is the Regge deficit angle at $e$ under the conformal ansatz and $\xi_0$ is the zero potential, is infinitely differentiable at $t = 0$.
background
The module isolates the hard analytic step for the full nonlinear Regge action: the second directional derivative at the flat potential must match the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
A vertex potential assigns a real conformal factor to each vertex. The line potential is the affine path $t \mapsto \xi_0 + t\xi$ through the zero (flat) potential. The deficit angle at a global edge $e$ is $2\pi$ minus the sum of local dihedral contributions from tetrahedra incident on $e$, evaluated under the conformal length ansatz.
Flat configuration supplies the local arccos-endpoint freeness needed so that deficitAngle, as a map on the space of potentials, is $C^\infty$ at the zero potential. That upstream smoothness fact is the only nontrivial geometric input here.
proof idea
Three short steps. First, the line map $t \mapsto$ linePotential$(K,\xi,t)$ is ContDiffAt $\top$ at $0$: rewrite as a product of coordinate maps and apply fun_prop on each affine coordinate. Second, deficitAngle as a function of the potential is ContDiffAt $\top$ at linePotential$(K,\xi,0)$; by linePotential_zero that basepoint is the zero potential, so the flat-configuration smoothness lemma for deficitAngle applies. Third, ContDiffAt.comp glues the two maps; a simp on Function.comp finishes.
why it matters
This is the base smoothness rung for the nonlinear Hessian chain. Downstream it feeds: differentiability of the first $t$-derivative of the deficit along the line at zero; the hinge-level package asserting deficit-line differentiability near zero for every potential; and the product-rule HasDerivAt step that differentiates the second factor in the action product rule.
In the broader Recognition geometry stack, the Regge action is the discrete curvature functional whose second variation at flat space should recover the incidence Hessian. Establishing $C^\infty$ of deficits along conformal lines is the analytic prerequisite before any second-derivative identity can be stated. The module doc frames the endpoint as equality of that second directional derivative with the canonical Hessian; this lemma clears the ContDiffAt hypothesis those later steps need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.