localDihedralDirectionalDerivativePackage_of_flat
plain-language theorem explainer
From a flat, incidence-consistent 3D triangulation, builds the package of directional derivatives of local tetrahedral dihedral angles under the conformal vertex-potential ansatz. Cited by anyone assembling the first-variation input for the nonlinear Regge action. The derivative field is the ordinary real derivative along the line potential; existence follows by C¹ smoothness at the zero potential plus the chain rule.
Claim. Let $K$ be a 3D triangulation with consistent incidence and a flat configuration. Then there is a local dihedral directional-derivative package: for every vertex potential direction $\eta$, tetrahedron $\tau$, and local edge index $f$, the map $t \mapsto \theta_f\bigl(K,\, t\cdot\eta,\,\tau\bigr)$ (dihedral angle under the conformal ansatz) is differentiable at $t=0$, and the package records that derivative.
background
This 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; the analytic work is to name the local derivative inputs until closed-form identities are fully expanded.
A vertex potential $\xi$ rescales squared edge lengths conformally. The line potential is the ray $t\mapsto t\cdot\eta$ through the zero (flat) potential. Local dihedral angles are read from the Cayley–Menger cofactor formula on those squared edges via tetDihedralAngleUnderConformal. The structure being inhabited packages, for each direction $\eta$, tetrahedron, and local face/edge index, both the numerical directional derivative at $t=0$ and a HasDerivAt witness.
Flatness supplies the nondegeneracy needed for the arccos/cofactor expressions to be $C^1$ at the zero potential (endpoint-free local arccos).
proof idea
The angleDeriv field is defined as the ordinary real derivative at $0$ of $t\mapsto$ dihedral angle of tetrahedron $\tau$, edge $f$, along the line potential in direction $\eta$.
For angle_hasDerivAt: invoke $C^1$ smoothness of the conformal dihedral map at the zero potential (from ReggeActionSmoothness, using flat local arccos nondegeneracy). Downgrade to DifferentiableAt and HasFDerivAt. Rewrite the base point as linePotential η 0 via the identity that the line at $0$ is the zero potential. Compose with linePotential_hasDerivAt_zero by HasFDerivAt.comp_hasDerivAt, then convert the composite derivative to the packaged real derivative.
why it matters
This definition is the concrete flat-case witness for the local dihedral cofactor/arccos derivative target. Downstream it is fed directly into reggeActionFirstVariationInput_of_conformalSchlaefliCancellation, which, given a conformal Schläfli cancellation hypothesis on this package, assembles the full first-variation input at the flat configuration.
In the Recognition geometry stack that input is the analytic half of the claim that the nonlinear Regge action has vanishing first variation at flat conformal potentials (Schläfli identities plus zero deficit). It does not itself touch the forcing chain T0–T8 or the RCL; it is pure discrete-geometry scaffolding for the Regge side of the continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.