LocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget
plain-language theorem explainer
Defines the near-flat chain-rule target for local dihedral angles under a conformal vertex potential: each angle derivative equals the closed-form squared-edge gradient dotted with the six conformal squared-edge speeds. Cited by the nonlinear Regge Hessian interface and by periodic six-tet gravity instances. Pure Prop packaging; no proof content.
Claim. For a 3D triangulation $K$, the target asserts: for every vertex potential $\xi$, eventually for all line parameters $t$ near $0$, and for every tetrahedron $\tau$ and local edge $f$, the $t$-derivative of the conformal dihedral angle equals $\sum_{k=0}^{5} \partial_{\ell_k}\theta_f(\ell(t))\cdot \ell_k'(t)$, where $\ell(t)$ are the six conformally scaled squared edge lengths and $\partial_{\ell_k}\theta_f$ is the closed-form squared-edge gradient of the tetrahedral dihedral angle.
background
This module packages the remaining analytic step for the nonlinear Regge Hessian: the second directional derivative of the Regge action at a flat potential must match the canonical incidence Hessian. The present definition is one link in that chain-rule stack.
Under the vertex-conformal ansatz, each local squared edge of tetrahedron $\tau$ scales as $\ell_f(\xi)=\ell_f^{(0)}\exp(\xi_u+\xi_v)$. The six-tuple of those lengths is the conformal squared-edge map. Dihedral angles are then composed with that map along the straight line potential $s\mapsto s\xi$.
The closed-form coordinate derivative dihedralAngle3SqClosedFormDeriv is the arccos chain-rule factor times the derivative of the cosine in squared-edge coordinates. The target says the actual geometric angle derivative equals that algebraic gradient contracted with the edge-length velocities, near the flat point $t=0$.
proof idea
No proof: this is a Prop-valued definition naming the desired identity. Downstream theorems discharge it. The flat-configuration theorem proves the target by rewriting the eventual quantifier and applying differentiability of the conformal edge map plus the closed-form angle gradient. A second combiner theorem takes this target together with a closed-form Schläfli-zero target and concludes the full local Schläfli-near-zero statement used by the Hessian interface.
why it matters
The nonlinear Regge Hessian proof interface needs a non-flat local angle chain rule before the second variation can be identified with the incidence Hessian. This definition is that interface atom: it isolates the squared-edge chain rule near zero without committing to a global flatness hypothesis in the statement itself.
It is consumed by localConformalSchlaefliAngleSqEdgeChainRuleNearZero_of_flatConfiguration, which supplies the identity on flat configurations, and by localConformalSchlaefliNearZero_of_sqEdgeChainRule_and_closedFormZero, which merges chain rule with closed-form Schläfli zero. Gravity code reuses it as the canonical periodic target on the encoded Freudenthal torus.
In the broader Recognition geometry stack this is pure classical Regge calculus bookkeeping (Cayley–Menger dihedrals, conformal edge scaling), not a forcing-chain step; it clears the analytic path from first variation to the quadratic Hessian form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.