LocalDihedralAngleLineDifferentiabilityNearZeroTarget
plain-language theorem explainer
For any finite 3D triangulation, every local tetrahedral dihedral angle along a conformal line through the flat potential is differentiable in a neighborhood of the origin. Deficit-angle expansions and the conformal Schläfli identity near zero take this Prop as analytic input. The body is a pure hypothesis package; a companion theorem discharges it under a flat configuration.
Claim. Let $K$ be a finite 3D triangulation. The target asserts: for every vertex conformal potential $\xi$, eventually as $t\to 0$, and for every tetrahedron $\tau$ and every local edge index $f\in\{0,\ldots,5\}$, the real map $s\mapsto\theta_{\tau,f}(s\cdot\xi)$ is differentiable at $t$, where $\theta_{\tau,f}$ is the dihedral angle of that local edge under the conformal squared-edge ansatz and $s\cdot\xi$ is the straight line through the zero potential in direction $\xi$.
background
The module isolates the hard analytic step in the nonlinear Regge Hessian: the second directional derivative of the Regge action at the flat conformal potential must match the canonical incidence Hessian. Vertex conformal potentials are real assignments on the vertices of $K$. The line through the flat (zero) potential in direction $\xi$ is the path $t\mapsto t\cdot\xi$.
Local dihedral angles under the conformal ansatz are computed from the Cayley–Menger cofactor formula on squared edge lengths of each tetrahedron. A global deficit angle at an edge is assembled from the incident local dihedral angles; differentiating that deficit therefore requires differentiability of each local contribution along the conformal line.
The doc-comment states the role directly: this is "the analytic input needed to expand the derivative of a deficit angle into the finite sum of derivatives of its incident local dihedral angles."
proof idea
Definitional packaging only: the declaration is a Prop-valued def, not a proved theorem. Its body is the universal quantification over directions $\xi$, the filter statement "eventually in a neighborhood of $0$", and pointwise DifferentiableAt of each local conformal dihedral-angle map. No lemmas are applied; discharge is deferred to the companion theorem that assumes a flat configuration and incidence consistency.
why it matters
This target sits on the critical path of the nonlinear Regge Hessian interface. Downstream, deficitLineDeriv_eq_neg_sum_local_nearZero uses it to write the derivative of each deficit as minus the sum of local dihedral derivatives near zero. That identity, together with an incidence-edge partition, feeds conformalSchlaefliNearZeroExpansion_of_angleDiff_and_partition, which establishes the conformal Schläfli expansion near the flat point.
The companion localDihedralAngleLineDifferentiabilityNearZero_of_flatConfiguration shows the target holds whenever the triangulation carries a flat configuration. Once the full second-chain-rule calculation is closed, the existing second-variation input follows and the directional Hessian at the flat potential equals the canonical incidence Hessian. In the broader Recognition geometry stack this is pure 3D Regge calculus (spatial $D=3$), not a forcing-chain step, but it is the remaining analytic gate for the nonlinear action Hessian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.