hingeDeficitSecondLineDifferentiability_of_deficit
plain-language theorem explainer
For an incidence-consistent 3D Regge triangulation, joint second-line differentiability of hinge measure and deficit along any potential ray at the flat point follows from the deficit half alone, since the hinge half holds unconditionally. Anyone wiring the nonlinear Regge Hessian interface cites this reduction. The proof is a one-line pair of the existing hinge differentiability lemma with the deficit hypothesis.
Claim. Let $K$ be a finite 3D Regge triangulation that is incidence-consistent. If, for every vertex potential $\xi$ and every edge $e$, the map $t \mapsto$ (first $t$-derivative of the edge deficit along the ray $t\xi$) is differentiable at $t=0$, then for every such $\xi$ and $e$ both the hinge-line derivative and the deficit-line derivative are differentiable at $t=0$.
background
The module isolates the hard remainder of the nonlinear Regge action: the second directional derivative of the action at the flat potential must equal the canonical incidence Hessian. Once that chain-rule calculation is in place, the existing second-variation input package follows at once.
A Triangulation3D is a finite abstract 3D Regge complex (vertex, edge, tetrahedron counts plus incidence and nondegenerate squared-edge data). Incidence consistency is the standing combinatorial hypothesis needed to define hinge measures under conformal rescaling. Along a ray $t\mapsto t\xi$ in the space of vertex potentials, one forms the first $t$-derivatives of the hinge measure and of the edge deficit; the target propositions ask that those first-derivative maps themselves be differentiable at the flat point $t=0$.
The hinge half of that joint condition is already proved for every incidence-consistent $K$. The deficit half is left as an explicit target proposition, because it is the analytic content still required by the second product-rule differentiation at the flat point.
proof idea
Term-mode packing, not a calculation. Introduce an arbitrary potential $\xi$ and edge $e$. The goal is the conjunction of hinge-line and deficit-line differentiability at zero. The first conjunct is supplied by the unconditional lemma that the hinge-line derivative is differentiable at zero (proved by unfolding the conformal hinge measure and the line potential). The second conjunct is exactly the deficit target hypothesis applied to the same $\xi$ and $e$. Package the pair and finish.
why it matters
This sits in the nonlinear Regge Hessian proof interface: the module's job is to make the second directional derivative of the full nonlinear Regge action at the flat potential equal the canonical incidence Hessian, after which ReggeActionSecondVariationInput is immediate. The joint hinge-and-deficit second-line differentiability condition is the sufficient regularity hypothesis for one more differentiation of the product-rule expression at the flat point. The present theorem removes the hinge half from the analytic burden, so only deficit second-line differentiability remains to be supplied. No downstream consumers are wired yet in the graph; the declaration is infrastructure for that remaining chain-rule step rather than a leaf of the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.