LocalDihedralDirectionalDerivativePackage
plain-language theorem explainer
Packages local directional derivatives of tetrahedral dihedral angles under the conformal vertex-potential ansatz on a finite 3D triangulation. Anyone assembling the first variation of the nonlinear Regge action via Schläfli cancellation cites this as the local analytic input. It is a structure: a derivative map plus HasDerivAt certificates at the flat potential t=0, not a proved identity.
Claim. For a finite 3D triangulation $K$, a local dihedral directional-derivative package consists of a map assigning to each vertex conformal potential $\eta$, tetrahedron $\tau$, and local edge slot $f\in\{0,\ldots,5\}$ a real number $D(\eta,\tau,f)$, together with the assertion that for every such triple the real map $t\mapsto$ (dihedral angle of $\tau$ at slot $f$ under the conformal squared-edge data of the line potential $t\eta$) is differentiable at $t=0$ with derivative $D(\eta,\tau,f)$.
background
The module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric route is Schläfli cancellation plus zero deficit; this structure records the precise local cofactor/arccos derivative input until those closed-form identities are fully expanded.
Vertex potentials are real assignments on the vertices of $K$. The line potential through the origin in direction $\eta$ is $t\mapsto t\eta$. Under the conformal ansatz, each tetrahedron's squared edge lengths are determined by those potentials, and dihedral angles are recovered from the Cayley-Menger cofactor formula (the concrete map tetDihedralAngleUnderConformal). Local edge slots of a tetrahedron are indexed by six labels.
Differentiability is Mathlib's HasDerivAt at $t=0$. Upstream, the same line-potential construction appears in the second-variation module; this local copy keeps the first-variation development independent.
proof idea
Structure definition, not a theorem. Two fields only: the candidate derivative map (vertex potential, tetrahedron, local edge slot) $\to\mathbb{R}$, and the universal family of HasDerivAt certificates that each conformal dihedral-angle path along a line potential is differentiable at the flat point with that value. No proof body and no tactics. Downstream lemmas take an inhabitant as a hypothesis and derive global deficit derivatives and Schläfli bookkeeping from it. Constructing a concrete instance from the closed-form cofactor/arccos formulae is the remaining analytic obligation flagged in the doc-comment.
why it matters
Local analytic hinge of the conformal first-variation pipeline. Downstream, the edge deficit directional derivative is assembled by summing the packaged local angle derivatives (with incidence signs); a companion theorem lifts the local HasDerivAt certificates to differentiability of the global deficit angle along each line potential. The exact Schläfli cancellation proposition and the incidence-bookkeeping proposition both take this package as a parameter. From cancellation one obtains a full deficit-angle directional-derivative package, which is the named input for vanishing of the first variation at the flat conformal potential.
In the Recognition geometry stack this sits between discrete Regge calculus and the continuum first-variation identity. It does not invoke the forcing chain T0–T8 or the Recognition Composition Law; it is pure 3D triangulation analysis supporting later curvature matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.