HingeDeficitSecondLineDifferentiabilityAtZeroTarget
plain-language theorem explainer
On an incidence-consistent 3D Regge triangulation, this Prop requires that the first t-derivatives of conformal hinge length and of deficit angle, taken along every conformal line through a vertex potential, are differentiable at the flat point t = 0. It is the exact differentiability interface needed before one more product-rule differentiation at the flat configuration. Downstream Hessian and product-rule theorems take it as a named hypothesis. The declaration is a pure Prop definition with no proof content.
Claim. For an incidence-consistent finite 3D Regge triangulation $K$, the target proposition is: for every vertex conformal potential $\xi$ and every edge $e$, both maps $t \mapsto$ (derivative of conformal hinge measure of $e$ along the line through $\xi$) and $t \mapsto$ (derivative of deficit angle of $e$ along the same line) are differentiable at $t = 0$.
background
The module isolates the remaining hard step for the full 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 supplied, the existing second-variation input package follows at once.
A Triangulation3D carries finite vertex/edge/tetrahedron counts with abstract incidence and nondegenerate squared-edge data. VertexPotential is a real assignment to vertices (conformal potentials). Along the conformal line $s \mapsto$ line potential through a fixed $\xi$, hingeLineDeriv is the ordinary one-variable derivative of the conformal hinge measure of an edge, and deficitLineDeriv is the corresponding derivative of the deficit angle. Incidence consistency is the standing geometric hypothesis on $K$.
The product-rule expression for the action derivative is built from these two one-variable factors; differentiating that product once more at the flat point needs both factors to be differentiable at $t = 0$.
proof idea
Pure Prop definition: no tactics and no lemmas. The body is the universal quantification over vertex potentials $\xi$ and edges $e$ of the conjunction of two DifferentiableAt statements, one for each line derivative evaluated at $0$. Downstream theorems discharge or consume the Prop by supplying those two conjuncts (hinge side often from a dedicated zero-point lemma; deficit side from a sibling target or flat-configuration argument).
why it matters
This interface sits on the second product-rule rung of the nonlinear Regge Hessian proof. It is consumed by the flat-configuration discharge theorem, by the reduction that assumes only deficit-side differentiability, by the theorem that turns a second-product geometric identity into the canonical-Hessian product-rule target, and by the pointwise HasDerivAt statement for the product-rule action derivative along a line.
In the module's own terms it is not a new physical assumption: it is the exact differentiability endpoint required before the second chain-rule calculation can finish. Closing it (via flat configuration or via the deficit-only sibling) is what lets the nonlinear directional Hessian equal the canonical incidence Hessian, which is the geometric content the second-variation package needs. It is local 3D Regge calculus infrastructure rather than a T0–T8 forcing step, but it is on the path that makes the discrete curvature action match its quadratic Hessian at flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.