SchlaefliPolySummandNormSumTarget
plain-language theorem explainer
Names the remaining closed-form target for tetrahedral Schläfli: after radical normalization, each of the six rational edge-summands sums to zero on every non-degenerate tetrahedron. Anyone finishing the local Schläfli package cites this Prop as the statement to discharge. It is a pure definition of that universal quantification, not a proof.
Claim. For every non-degenerate tetrahedron $T$ (positive squared edge lengths and positive Cayley–Menger $3$-volume) and every fixed edge index $k\in\{0,\ldots,5\}$, $\sum_{e=0}^{5} S_{\mathrm{norm}}(a_T,e,k)=0$, where $S_{\mathrm{norm}}$ is the rationalized Schläfli summand (cofactor polynomials with the arccos radical removed) and $a_T$ are the squared edge lengths of $T$.
background
The module ties explicit Cayley–Menger and dihedral derivative formulae to the local tetrahedral Schläfli package. The hard residue is a single closed-form identity rather than an external field.
A non-degenerate tetrahedron carries six positive squared edge lengths whose Cayley–Menger $3$-volume is positive. The rationalized summand schlaefliPolySummandNorm is the pure rational expression obtained after clearing the arccos radical via the cofactor discriminant: up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, it matches the original polynomial-cofactor Schläfli term. Edge indices run over $\mathrm{Fin},6$.
The classical Schläfli differential relation equates a weighted sum of dihedral-angle derivatives to a volume derivative. After closed-form differentiation and radical normalization, that relation becomes six rational finite sums, one per fixed edge slot $k$.
proof idea
No proof: the declaration is a Prop abbreviation. It packages the universal statement “for all non-degenerate $T$ and all $k:\mathrm{Fin},6$, the six-term sum of rationalized summands vanishes.” Downstream, the actual proof expands the $\mathrm{Fin},6$ sum via the explicit six-term identity, invokes non-vanishing of dihedral cofactor products on non-degenerate tets, clears denominators, and finishes by ring normalization of the cofactor polynomials.
why it matters
This is the named post-radical target the module’s doc flags as the remaining content. The parent theorem schlaefliPolySummandNorm_sum_eq_zero is exactly the claim that this Prop holds; the six-term expansion lemma is the first rewrite step in that proof. Closing it completes the bridge from Cayley–Menger/dihedral closed forms to the local tetrahedral Schläfli package, so later geometry and Regge-type arguments can cite a fully rational identity instead of an implicit transcendental relation. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is pure $3$-simplex differential geometry inside the RS geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.