localDihedralDirectionalDerivativePackage_of_lengthChain
plain-language theorem explainer
Packages the edge-length chain-rule formula for dihedral-angle directional derivatives into the local analytic interface used by the Regge first-variation argument. Anyone assembling Schläfli cancellation or the first-variation input from a length-chain package cites this. Construction is a pure field assignment: derivative values are the closed Schläfli chain-rule expressions, and the HasDerivAt witness is inherited from the length-chain package.
Claim. Given a finite 3D Regge triangulation $K$ with incidence-consistent data and a local angle-length chain-rule package $L$ (supplying $\mathrm{HasDerivAt}$ for each tetrahedron dihedral angle along the conformal line potential), form the local dihedral directional-derivative package whose derivative values equal the Schläfli edge-length chain-rule expressions and whose derivative certificates are those of $L$.
background
The module targets vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; until the closed-form local identities are fully expanded, the analytic content is packaged as named input structures.
A triangulation $K$ carries abstract incidence (vertices, edges, tets) and a nondegenerate squared-edge tuple on every tetrahedron. Incidence consistency is the standing hypothesis that makes the local Schläfli data well-defined. Under the conformal ansatz one deforms edge lengths by a vertex potential $\eta$ along the line $t\mapsto$ linePotential$(K,\eta,t)$, and studies dihedral angles of each tet at $t=0$.
The local dihedral directional-derivative package is the precise cofactor/arccos target: a function angleDeriv together with a HasDerivAt certificate for each tet face. The length-chain package specializes those values to the closed Schläfli chain rule $\sum_k(\mathrm{dihedralDeriv},f,k)\cdot(\mathrm{localEdgeLengthDirectionalDeriv},\eta,\tau,k)$, leaving only the HasDerivAt obligation that ties the actual arccos angle to that formula.
proof idea
One-line structure constructor. Set angleDeriv to the closed-form localAngleLengthChainDeriv (the sum of Schläfli dihedral cofactors times local edge-length directional derivatives). Copy angle_hasDerivAt verbatim from the supplied length-chain package $L$. No new analysis is performed.
why it matters
This is the bridge from length-chain analytic data into the interface expected by the first-variation pipeline. Downstream, conformalSchlaefliCancellation_of_lengthChain_of_bookkeeping takes the resulting package plus incidence bookkeeping and obtains conformal Schläfli cancellation. The same package is threaded through reggeActionFirstVariationInput_of_incidenceBookkeeping and the edge-slot variant to assemble the full first-variation input at a flat configuration.
On the gravity side, canonicalPeriodicLocalDihedralDerivativePackage for the periodic Freudenthal torus is built in this shape, so the six-tet cubic Dirichlet instance inherits the same local derivative interface. Within the Recognition geometry stack this sits under the Regge-action first-variation program that supports continuum limits and curvature bookkeeping; it does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it is part of the discrete-geometry substrate those continuum claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.