snorm_zero_3_0
plain-language theorem explainer
For the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand at edge index 3 and squared-edge coordinate 0 vanishes. Discrete-geometry and RS gravity workers cite it as one cell of the 6×6 certificate table that closes the local length-chain derivative. The proof rewrites the summand as an explicit rational function of the six squared edges, unfolds the cofactor polynomials, and finishes by numeric evaluation.
Claim. Let $a$ be the squared-edge 6-tuple of a Freudenthal tetrahedron in the unit cube (three unit step edges, two face diagonals, one body diagonal). The rationalized Schläfli summand of $a$ at edge index $e=3$ and squared-edge coordinate $k=0$ equals $0$.
background
The module certifies a full $6\times 6$ evaluation of the rationalized Schläfli summand on the Freudenthal tetrahedron, then feeds those values into a closed-form table for the local length-chain derivative of the dihedral angle.
A Freudenthal tetrahedron tiles the unit cube; its squared-edge tuple is fixed: three edges of squared length $1$, two face diagonals of squared length $2$, and one body diagonal of squared length $3$. Dihedral geometry is encoded via Cayley–Menger cofactors: each cofactor is an explicit polynomial in the six squared edges, and partials of those polynomials appear in the summand numerator. Opposite Cayley–Menger vertex pairs label which cofactors sit in the denominator for a given edge.
The rationalized summand is the pure rational expression obtained after clearing the arccos radical by the cofactor discriminant. Up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, it is the quantity evaluated here.
proof idea
Term-mode arithmetic certificate. 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 edge $3$. Simplify with the explicit cofactor polynomial and cofactor-partial match tables. Finish with norm_num, which reduces the concrete rational expression in the six numeric edge squares to $0$.
why it matters
One of the thirty-six cell certificates that assemble into the lookup-table equality freudenthalSchlaefliPolySummandNorm_eq_table. That table is the bridge from abstract Schläfli–Cayley–Menger calculus to the closed-form coefficient list used by freudenthalLocalPairClosedFormSchlaefliCoeff and the induced dihedralClosedDerivLength table.
In the RS gravity stack, Freudenthal length-chain endpoints supply the discrete geometric input for local curvature and dihedral response on the cubic lattice. A vanishing cell is not decorative: it records that the length derivative of a particular dihedral contribution is identically zero on this edge–coordinate pair, which simplifies the closed-form table and removes a term from downstream gravity identities. The result is fully proved (no sorry); it closes one scaffold cell rather than leaving an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.