localConformalSchlaefliClosedFormZeroNearZero
plain-language theorem explainer
For any 3D triangulation, the closed-form six-edge Schläfli sum vanishes on every conformally deformed tetrahedron along the flat-potential line, for all sufficiently small step sizes. Discrete-gravity and Regge-calculus workers cite it when the second variation must stay inside the nondegenerate cone. The proof builds a nondegenerate tet package near t = 0 and applies the algebraic six-edge Schläfli identity.
Claim. Let $K$ be a 3D triangulation. For every vertex potential direction $\xi$, there is a neighbourhood of $t=0$ such that for every tetrahedron $\tau$ and every edge index $k\in\{0,\ldots,5\}$, $$\sum_{f=0}^{5}\sqrt{\ell_f(t,\tau)}\,\partial_{\ell_k}\theta_f^{\mathrm{cl}}\bigl(\ell(t,\tau)\bigr)=0,$$ where $\ell(t,\tau)$ is the six-tuple of conformally scaled squared edge lengths of $\tau$ along the line potential $t\xi$, and $\theta_f^{\mathrm{cl}}$ is the closed-form dihedral angle in those squared-edge coordinates.
background
The module isolates the hard second-variation step for the nonlinear Regge action: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. The present target is the algebraic half of that identity under the local conformal ansatz.
A vertex potential $\xi$ deforms edge lengths by scaling; the line potential is the ray $t\mapsto t\xi$ through the flat configuration. For each tetrahedron $\tau$, conformalTetSqEdges packages the six conformally scaled squared-edge coordinates. Near $t=0$ those coordinates stay positive and the Cayley–Menger determinant stays positive, so the deformed tet remains inside the nondegenerate cone.
Classical Schläfli says $\sum_e \ell_e,d\theta_e=0$ for any first-order deformation of a Euclidean tetrahedron. Here the same identity is needed in closed form, differentiated with respect to each squared-edge coordinate, evaluated on the conformal six-tuple along the line.
proof idea
Fix a direction $\xi$. Rewrite the filter quantifier over tetrahedra, then for each $\tau$ pull the eventual Cayley–Menger positivity lemma cm3_conformalTetSqEdges_line_pos_eventually. On that neighbourhood, for each edge index $k$, assemble a NonDegenerateTet whose squared edges are the conformal six-tuple at step $t$, with edge positivity from conformalLocalSqEdge_line_pos and CM positivity from the filter witness. Apply SchlaefliTetrahedronProof.tetraSchlaefliSixEdgeClosedForm to that package and the index $k$; a short simpa rewrites the closed-form dihedral derivative and the conformal edge map back to the target sum.
why it matters
This discharges the closed-form Schläfli-zero half of the local conformal identity for an arbitrary triangulation, which is a prerequisite for the nonlinear directional Hessian equaling the canonical incidence Hessian (the module's stated endpoint). Downstream, canonicalPeriodicLocalConformalSchlaefliClosedFormZeroNearZeroTarget specialises it to every canonical periodic Freudenthal torus used in the physical six-tet cubic Dirichlet gravity instance: "the closed-form algebraic Schläfli-zero half of the local conformal identity is closed for every canonical periodic Freudenthal torus."
In the broader Recognition geometry stack this keeps the discrete curvature variation inside the nondegenerate cone near flat space, so the second-variation chain can feed continuum limits without an extra nondegeneracy hypothesis. It does not by itself finish the Hessian equality; sibling targets still handle first-order tangency and linearisation of the action derivative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.