localConformalSchlaefliAngleSqEdgeChainRuleNearZero_of_flatConfiguration
plain-language theorem explainer
Near a flat configuration on an incidence-consistent 3D triangulation, each local dihedral angle along a conformal line of vertex potentials has derivative equal to the closed-form squared-edge gradient contracted with the six edge derivatives. Discrete-gravity and Regge-calculus workers cite this when closing the nonlinear Hessian at the flat point. The proof is a filter-local Fréchet chain rule: compose the dihedral map's derivative with the conformal squared-edge path, then expand in Pi coordinates.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation that admits a flat configuration. Then for every vertex potential $\xi$, eventually for all line parameters $t$ near $0$, and for every tetrahedron $\tau$ and edge index $f\in\{0,\ldots,5\}$, $$\frac{d}{ds}\Big|_{s=t}\theta_{\tau,f}\bigl(\phi_{K,\xi}(s)\bigr)=\sum_{k=0}^{5}\partial_{a_k}\Theta_3\bigl(a(t)\bigr)\,a_k'(t),$$ where $a(s)\in\mathbb{R}^6$ are the conformal squared edge lengths of $\tau$ along the line potential through $\xi$, and $\Theta_3$ is the closed-form dihedral angle in squared-edge coordinates.
background
This module isolates the hard second-variation calculation for the nonlinear Regge action: the second directional derivative of the action at a flat potential must match the canonical incidence Hessian. The present target is one half of that chain-rule endpoint, namely the first derivative of local dihedral angles under conformal deformations, written in squared-edge coordinates.
Squared edge lengths of a tetrahedron are the type SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The map $\Theta_3$ is the closed-form dihedral angle as a function of those six coordinates; its coordinate partials are dihedralAngle3SqClosedFormDeriv. A local conformal deformation is generated by a vertex potential $\xi$ along the straight line $\phi_{K,\xi}(s)$, which induces six conformal squared-edge paths on each tetrahedron $\tau$.
The target proposition asserts that, near the flat point $t=0$, the ordinary derivative of each conformal dihedral angle equals the pairing of those closed-form partials with the six edge-path derivatives. Upstream continuity and non-degeneracy facts supply $\mathrm{ContDiffAt}$ of $\Theta_3$ on non-degenerate tets and positivity of conformal edges along the line.
proof idea
Fix a vertex potential $\xi$. Work eventually near $t=0$, then fix tetrahedron $\tau$ and face index $f$. Filter-upwards with two eventualities: positivity of the six conformal squared edges along the line, and the endpoint-free hypothesis needed for the dihedral cosine.
Package the conformal squared edges at parameter $t$ into a non-degenerate tet $T$. Let $F$ be $\Theta_3(\cdot,f)$ and let $v$ be the $\mathbb{R}^6$-velocity of the conformal edge path at $t$. ContDiffAt of $F$ at $T$ (from the first-variation library, using the endpoint-free fact) yields DifferentiableAt and HasFDerivAt. The edge path itself has HasDerivAt with derivative $v$.
Compose via HasFDerivAt.comp_hasDerivAt. Expand the Fréchet action on $v$ as a sum over Pi.single basis vectors, replace each coordinate derivative by the closed-form partial (fderiv_dihedralAngle3Sq_apply_single), and rewrite to the stated sum. Simp closes the identification with the conformal dihedral derivative.
why it matters
The module frames this as the exact endpoint of the second chain-rule calculation for the nonlinear Regge Hessian: once the local angle derivatives match the squared-edge gradient pairing, ReggeActionSecondVariationInput follows and the second directional derivative at the flat potential equals the canonical incidence Hessian.
Downstream, canonicalPeriodicLocalConformalSchlaefliAngleSqEdgeChainRuleNearZeroTarget instantiates the same identity on every canonical periodic Freudenthal torus (the physical six-tet cubic Dirichlet setting). That closes the non-flat squared-edge half of the local conformal Schläfli identity near the flat point for the gravity stack.
In the broader Recognition geometry layer this is pure discrete differential geometry (Regge calculus / Schläfli), not a forcing-chain step, but it is required scaffolding for curvature and action second variation on the triangulated spatial slices that carry the eight-tick and $D=3$ structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.