LocalConformalSchlaefliNearZeroTarget
plain-language theorem explainer
Local near-flat Schläfli identity along conformal vertex-potential lines: for every direction ξ, near t = 0 the length-weighted sum of dihedral-angle derivatives over each tetrahedron's six edges vanishes. Hessian-proof authors cite it as the local target that closes the second chain-rule step for the nonlinear Regge action. It is a Prop definition packaging that identity, not a proved theorem.
Claim. For a 3D triangulation $K$, the local near-flat Schläfli target asserts: for every vertex potential $\xi$, eventually for all $t$ near $0$, and for every tetrahedron $\tau$, $$\sum_{f=0}^{5} \ell_f(t)\,\partial_t\theta_f(t)=0,$$ where $\ell_f(t)=\sqrt{\text{conformal local squared edge}}$ and $\theta_f$ is the dihedral angle under the conformal ansatz along the line $s\mapsto s\xi$ through the flat potential.
background
In Regge calculus the classical Schläfli identity on a simplex equates a first-order variation of edge lengths and opposite dihedral angles: $\sum \ell_e,d\theta_e=0$. The nonlinear Hessian program needs this along conformal deformations of a flat triangulation, but only near the flat point, where the nondegenerate chart supplies a valid tetrahedral domain.
A conformal line is $t\mapsto t\xi$ through the zero (flat) vertex potential. Local squared edges scale by $\exp(\xi_u+\xi_v)$; dihedral angles come from the Cayley-Menger cofactor formula on those squared edges. The ambient module isolates the remaining hard calculation: the second directional derivative of the Regge action at the flat potential must equal the canonical incidence Hessian. Once that chain-rule endpoint is supplied, the existing second-variation input follows immediately.
proof idea
Pure Prop definition, not a theorem. The body quantifies over all vertex potentials $\xi$, requires the identity eventually in a neighborhood of $t=0$ (filter eventually in $\mathrm{nhds},0$), and for each tetrahedron sums edge length times dihedral derivative over the six local edges. No tactics or lemmas are applied here; discharge is deferred to downstream theorems that combine a squared-edge chain rule with a closed-form zero identity.
why it matters
Module goal: second directional derivative at flat equals the canonical incidence Hessian. This target is the local Schläfli piece of that calculation. It is proved from chain-rule and closed-form-zero targets by localConformalSchlaefliNearZero_of_sqEdgeChainRule_and_closedFormZero, then fed into the weighted-deficit derivative eventually-zero and stationary targets that unlock the Hessian. A gravity-side specialization instantiates it on the canonical periodic Freudenthal torus. In the RS geometry stack this is discrete-curvature scaffolding for continuum matching, not a direct T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.