tetDihedralAngleUnderConformal_line_contDiffAt_zero_of_flatConfiguration
plain-language theorem explainer
Along any straight line of conformal vertex potentials through the origin, each local tetrahedral dihedral angle is infinitely differentiable at the flat point. Anyone proving second-variation or Hessian identities for the nonlinear Regge action under the conformal ansatz will cite this. The argument is chain rule: C^∞ of the line map composed with C^∞ of the angle map at the zero potential, using flatness to free the arccos endpoint.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat. Fix a vertex potential $\xi$, a tetrahedron $\tau$, and a local edge index $f\in\{0,\ldots,5\}$. The real map $t\mapsto$ (dihedral angle of $\tau$ at $f$ under the conformal edge lengths induced by the line potential $t\xi$) is $C^\infty$ at $t=0$.
background
This module isolates the hard endpoint of the nonlinear Regge second-variation calculation: the second directional derivative of the action 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.
The conformal ansatz deforms squared edge lengths by a vertex potential $\xi$. The local dihedral angle of tetrahedron $\tau$ at edge $f$ is read from the Cayley–Menger cofactor formula on those squared edges. The line potential is the straight path $t\mapsto t\xi$ in potential space; at $t=0$ it is the zero potential.
Flatness of the configuration supplies a local arccos-endpoint-free hypothesis at each tetrahedron edge, which is the hypothesis needed for infinite differentiability of the dihedral-angle map at the zero potential.
proof idea
Three steps. First, the line potential $t\mapsto t\xi$ is $C^\infty$ at $0$: rewrite as a product of coordinate maps and apply fun_prop on each component. Second, the map sending a potential $\eta$ to the conformal dihedral angle at $(\tau,f)$ is $C^\infty$ at the zero potential, by the existing smoothness lemma for that angle, fed the flat configuration’s local arccos-endpoint-free fact (and rewritten via the identity that the line potential at $0$ is zero). Third, compose the two $C^\infty$ maps at $t=0$ and unfold function composition.
why it matters
This is a local smoothness brick for the nonlinear Regge Hessian program. Its sole downstream consumer is the theorem that packages local dihedral-angle line differentiability near zero for a flat configuration, which in turn feeds the chain-rule path toward equality of the second directional derivative with the canonical incidence Hessian.
In the Recognition geometry stack, Regge action and its second variation sit under the discrete curvature side of the forcing chain (spatial dimension $D=3$, eight-tick structure). The result does not itself compute the Hessian; it only guarantees that the angle factors along conformal lines are smooth enough at the flat point for second derivatives to exist and for the remaining algebraic identification to be well-posed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.