snorm_1_3
plain-language theorem explainer
For the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand at edge index 1 and squared-edge coordinate 3 equals −4. Gravity and discrete-geometry workers cite it when assembling the closed-form dihedral length-derivative table. The proof rewrites the summand as numerator over denominator, unfolds the Freudenthal edge lengths and opposite Cayley–Menger vertices, then finishes by polynomial simplification and numeric normalization.
Claim. On the Freudenthal tetrahedron squared-edge data (three unit edges, two face diagonals, one body diagonal), the rationalized Schläfli summand for edge $e=1$ and squared-edge coordinate $k=3$ equals $-4$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on every Freudenthal tetrahedron in the unit cube, and the induced closed-form table for the local dihedral length derivative.
A Freudenthal tetrahedron has squared-edge tuple $(1,2,3,1,2,3)$: three unit steps, two face diagonals, and one body diagonal. The Schläfli identity expresses dihedral-angle derivatives in terms of Cayley–Menger cofactors of that tuple. The rationalized summand removes the arccos radical via the cofactor discriminant, leaving a pure rational expression (numerator over a product of two diagonal cofactors) up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$.
Opposite Cayley–Menger vertex pairs label which cofactors enter each edge’s summand. Explicit polynomial normal forms for those cofactors and their partials with respect to squared-edge coordinates make the evaluation purely algebraic.
proof idea
Term-mode proof. Rewrite the summand via the identity that it equals numerator over denominator. Unfold the numerator and denominator definitions, the Freudenthal squared-edge assignment, and the opposite-vertex map for edge 1. Simplify with the explicit cofactor polynomial and cofactor-partial match tables, then close by norm_num, which evaluates the resulting rational expression to $-4$.
why it matters
One cell of the $6\times 6$ Freudenthal Schläfli-summand table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table matches every $(e,k)$ against the lookup table by case-splitting; this declaration discharges the $(1,3)$ case. That table feeds the closed-form coefficients of the local dihedral length derivative on the Freudenthal triangulation, the discrete geometric input to the Recognition gravity length-chain endpoint certificates. No forcing-chain landmark (T5–T8) is invoked directly; the result is pure tetrahedral algebra supporting the gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.