LocalConformalSchlaefliClosedFormZeroNearZeroTarget
plain-language theorem explainer
Names the local closed-form Schläfli vanishing identity under a conformal vertex-potential deformation of a 3D triangulation: near the flat line parameter t=0, for every tetrahedron and every squared-edge coordinate, the length-weighted sum of closed-form dihedral derivatives is zero. Downstream Hessian and periodic gravity instances cite this Prop as the algebraic non-flat Schläfli target. The body is a pure predicate definition, not a proof.
Claim. For a 3D triangulation $K$, the target asserts: for every vertex potential $\xi$, eventually as $t\to 0$, and for every tetrahedron $\tau$ and every edge index $k\in\{0,\ldots,5\}$, $$\sum_{f=0}^{5}\sqrt{\ell_f^{2}(\xi,t;\tau)}\,\partial_{a_k}\theta_f\bigl(a(\xi,t;\tau)\bigr)=0,$$ where $\ell_f^{2}$ are the conformally scaled local squared edges along the line potential $t\xi$, $a(\xi,t;\tau)$ is the six-tuple of those squared edges, and $\partial_{a_k}\theta_f$ is the closed-form derivative of the dihedral angle at edge $f$ with respect to squared-edge coordinate $k$.
background
The module isolates the hard endpoint of the nonlinear Regge Hessian calculation: the second directional derivative of the Regge action at the flat potential must match the canonical incidence Hessian. Once that chain-rule identity is supplied, the existing second-variation input package follows at once.
A vertex potential $\xi$ deforms edge lengths conformally: the local squared edge $f=(u,v)$ in tetrahedron $\tau$ scales by $\exp(\xi_u+\xi_v)$. The line potential is the ray $t\mapsto t\xi$ through the flat configuration. Dihedral angles are treated in squared-edge coordinates via a closed-form arccos chain rule: the derivative of $\theta$ is $-(1-\cos^{2}\theta)^{-1/2}$ times the closed-form cosine derivative.
The classical Schläfli relation for a tetrahedron says length-weighted dihedral variations sum to zero. Here that identity is restated algebraically on the conformally deformed squared-edge tuple, restricted to a neighborhood of $t=0$ where the tetrahedron stays in the nondegenerate cone.
proof idea
No proof: this is a Prop-valued definition fixing the exact predicate later theorems must discharge. The body quantifies over all vertex potentials $\xi$, requires the identity eventually in a neighborhood of $t=0$, and for each tetrahedron and each differentiation index $k$ asserts that the sum over the six local edges of $\sqrt{\text{conformal local squared edge}}\times(\text{closed-form dihedral derivative in squared-edge coordinates})$ vanishes. Upstream ingredients are only the conformal edge maps, the line potential, and the closed-form dihedral derivative; they appear as data inside the predicate, not as lemmas applied here.
why it matters
This target is the algebraic non-flat Schläfli identity once conformal tetrahedra remain nondegenerate near $t=0$. The sibling theorem localConformalSchlaefliClosedFormZeroNearZero is exactly the claim that every triangulation satisfies the target. Combined with the squared-edge chain-rule target, it yields the full local conformal Schläfli-near-zero package via localConformalSchlaefliNearZero_of_sqEdgeChainRule_and_closedFormZero.
In the gravity layer, the canonical periodic six-tet cubic Dirichlet instance specializes the same Prop to the encoded periodic Freudenthal torus, so the continuum Hessian story inherits a concrete discrete Schläfli zero. Within the module's program, discharging this identity is part of closing the nonlinear directional Hessian at the flat potential against the canonical incidence Hessian, the remaining hard calculation flagged in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.