ConformalSchlaefliAlongLineExpansionTarget
plain-language theorem explainer
Defines the global-to-local expansion identity for the weighted deficit-derivative sum along any conformal line on an incidence-consistent 3D triangulation. Anyone assembling the conformal Schläfli identity for the nonlinear Regge Hessian cites this Prop. It is pure definitional packaging: incidence reindexing, hinge-to-local-edge matching, and deficit-as-minus-angle-derivatives, with no proof obligation attached.
Claim. For an incidence-consistent 3-triangulation $K$, the following holds for every vertex potential $\xi$ and every $t\in\mathbb{R}$: $$\sum_e h_e(\xi_t)\,\delta'_e(\xi,t)=-\sum_\tau\sum_{f=1}^{6}\ell_{\tau,f}(\xi_t)\,\frac{d}{ds}\Big|_{s=t}\theta_{\tau,f}(\xi_s),$$ where $h_e$ are conformal hinge measures, $\delta'_e$ are line derivatives of edge deficits, $\ell_{\tau,f}=\sqrt{\text{local conformal squared edge}}$, and $\theta_{\tau,f}$ are tetrahedral dihedral angles under the vertex-conformal ansatz along the line $\xi_s$.
background
The module isolates the remaining hard step of the nonlinear Regge Hessian: the second directional derivative of the Regge action at the flat potential must match the canonical incidence Hessian. Once that chain-rule calculation is in hand, the existing second-variation input package follows at once.
A conformal line is the one-parameter family of vertex potentials $s\mapsto\xi_s$ obtained by scaling along a fixed direction $\xi$. Under the vertex-conformal ansatz, each local squared edge in tetrahedron $\tau$ scales by $\exp(\xi_u+\xi_v)$ (the local conformal squared-edge data). Hinge measures and tetrahedral dihedral angles are the corresponding conformal deformations of the classical Regge geometric quantities.
The classical Schläfli identity relates hinge lengths times deficit derivatives to edge lengths times dihedral-angle derivatives. This target lifts that identity to the conformal line at an arbitrary parameter $t$, including the non-flat incidence bookkeeping that reindexes global edges to the six local edge slots of each tetrahedron.
proof idea
Definitional Prop, not a proved theorem. The body is the quantified equality itself: left-hand side is the global sum over edges of conformal hinge measure times deficit line derivative; right-hand side is minus the double sum over tetrahedra and their six edge slots of local conformal edge length times the $t$-derivative of the conformal dihedral angle. No tactics, no lemmas applied. Downstream proofs discharge or assume this Prop as a named hypothesis.
why it matters
This is the non-flat expansion/reindexing half of the conformal Schläfli identity along lines. The combiner theorem conformalSchlaefliAlongLine_of_expansion_and_local takes this target together with the local near-flat Schläfli target and concludes the full conformal Schläfli-along-line target used by the nonlinear directional Hessian argument.
It is also specialized in the gravity layer to the canonical periodic Freudenthal torus, as the periodic non-flat expansion target for six-tet cubic Dirichlet instances. In the module's own framing, closing the Hessian chain (second directional derivative equals canonical incidence Hessian) is the exact endpoint of the second chain-rule calculation; this Prop carves out the incidence and deficit-derivative bookkeeping so that the remaining local analytic work can be stated separately.
No direct appeal to T0–T8 or the Recognition Composition Law; the link is geometric, through the Regge action whose second variation feeds continuum gravity limits in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.