snorm_zero_5_4
plain-language theorem explainer
The rationalized Schläfli summand for the Freudenthal unit-cube tetrahedron vanishes at edge index 5 and squared-edge coordinate 4. Gravity and discrete-geometry workers cite it when assembling the full 6×6 summand table that feeds the closed-form dihedral length derivative. The proof rewrites the summand as a ratio of cofactor polynomials, unfolds the Freudenthal edge tuple, and finishes by numeric simplification to zero.
Claim. For the squared-edge 6-tuple of a Freudenthal tetrahedron in the unit cube, the rationalized Schläfli summand (cofactor form with the arccos radical removed) at edge index $e=5$ and squared-edge coordinate $k=4$ equals $0$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on the Freudenthal tetrahedron and the induced closed-form table for the local dihedral length derivative. A Freudenthal tetrahedron in the unit cube has squared edges given by the fixed tuple with three unit steps, two face diagonals, and one body diagonal.
The rationalized Schläfli summand is the pure rational expression obtained after clearing the arccos radical via the Cayley–Menger cofactor discriminant; up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, it equals the original polynomial-cofactor summand. Its numerator and denominator are built from the explicit cofactor polynomials $\mathrm{cmCofactor3Poly}$ and their partials with respect to squared-edge coordinates, indexed by the pair of Cayley–Menger vertices opposite the chosen edge.
Upstream, those cofactors are given in closed polynomial normal form, and the opposite-vertex map sends each of the six edges to the complementary pair in the $5\times 5$ Cayley–Menger matrix.
proof idea
Term-mode proof by direct evaluation. Rewrite the summand via the identity that expresses it as numerator over denominator. Unfold the numerator, denominator, the Freudenthal squared-edge tuple, and the opposite-vertex map for the edge. Simplify with the explicit cofactor polynomial and cofactor-partial match tables, then discharge the resulting rational arithmetic by norm_num, obtaining zero.
why it matters
One cell of the $6\times 6$ Freudenthal summand table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table matches every $(e,k)$ against a lookup table by case analysis; this declaration supplies the $(5,4)$ case (value $0$). That table in turn underwrites the closed-form coefficients of the local dihedral length derivative on the Freudenthal triangulation, the discrete geometric input used in the gravity length-chain endpoint certificates. Within Recognition Science the Freudenthal cube triangulation is the standard spatial discretization compatible with the forced $D=3$ and eight-tick octave structure; exact vanishing of selected summands simplifies the length-chain algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.