LocalAngleLengthChainRulePackage
plain-language theorem explainer
Packages the local analytic obligations that each tetrahedral dihedral angle, deformed along a conformal line of vertex potentials, is differentiable at t=0 with derivative equal to the closed-form edge-length chain rule. Cited by Schläfli-cancellation theorems and the six-tet cubic Dirichlet instance on the periodic Freudenthal torus. Pure structure definition: no proof body, only the HasDerivAt field bundle.
Claim. For an incidence-consistent 3D triangulation $K$, a local angle-length chain-rule package is a record asserting: for every vertex potential $\eta$, every tetrahedron $\tau$, and every local edge index $f\in\{0,\ldots,5\}$, the real map $t\mapsto$ (dihedral angle of $\tau$ at $f$ under the conformal squared-edge data of the linear potential path through $\eta$ at time $t$) is differentiable at $t=0$, with derivative equal to the closed-form length chain-rule value at $(\eta,\tau,f)$.
background
This module targets the 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 justify differentiating the local dihedral angles under the conformal ansatz.
The dihedral angle under conformal deformation is computed from the Cayley-Menger cofactor formula on squared-edge data of a tetrahedron. A vertex potential $\eta$ is deformed along the straight line $t\mapsto$ linePotential$(\eta,t)$ in potential space. The closed-form length chain-rule derivative is the candidate value of that directional derivative at $t=0$.
The structure packages exactly the remaining local obligation: each such angle map has a derivative at zero equal to that closed-form value. Incidence consistency of the triangulation is a parameter hypothesis, not part of the field data.
proof idea
Structure definition with empty proof body. The single field is a universal HasDerivAt statement comparing the actual cofactor/arccos angle path to the named closed-form length chain-rule derivative at time zero. Instantiation is deferred: the sibling constructor from the squared-edge chain-rule package fills the field by reducing length derivatives to squared-edge derivatives via the explicit cofactor formulas.
why it matters
This is the length-side analytic interface for the first-variation argument. Downstream, it converts into a local dihedral directional-derivative package, which then feeds the conformal Schläfli cancellation theorem once incidence bookkeeping is supplied. The gravity layer builds a canonical instance on the periodic Freudenthal torus (six-tet cubic Dirichlet setting).
In the Recognition geometry stack this sits under the D=3 forcing (T8) and the discrete Regge path to the Einstein-Hilbert sector: without local differentiability of dihedral angles under conformal edge scaling, the first-variation identity cannot be stated in Lean. It does not itself close the global vanishing theorem; it isolates the local chain-rule step so Schläfli plus zero deficit can finish the job.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.