snorm_3_4
plain-language theorem explainer
On the Freudenthal tetrahedron squared-edge data, the rationalized Schläfli summand at edge index 3 and squared-edge coordinate 4 equals -2. Gravity and discrete-geometry workers cite this as one cell of the 6×6 certificate table that closes the local dihedral length derivative. The proof rewrites the summand as a numerator over denominator, unfolds the Freudenthal edges and opposite Cayley–Menger vertices, simplifies the cofactor polynomials, and finishes by numeric normalization.
Claim. Let $a$ be the squared-edge 6-tuple of a Freudenthal tetrahedron in the unit cube (three unit edges, two face diagonals, one body diagonal). The rationalized Schläfli summand of $a$ at edge index $e=3$ and squared-edge coordinate $k=4$ equals $-2$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on Freudenthal tetrahedra, and the induced closed-form table for the local dihedral length derivative used in the gravity length-chain.
A Freudenthal tetrahedron in the unit cube has fixed squared edges $a$: three unit steps, two face diagonals of squared length 2, and one body diagonal of squared length 3. The Schläfli identity for a tetrahedron expresses dihedral-angle variation in terms of edge lengths; after clearing the arccos radical via the Cayley–Menger cofactor discriminant, each summand becomes a pure rational function of the squared edges (the “norm” form), up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$.
Numerator and denominator are built from the explicit degree-3 Cayley–Menger cofactor polynomials and their partials in the squared-edge coordinates, with opposite vertex pairs read off the edge index. Upstream lemmas supply the polynomial normal forms, the opposite-vertex map, and the identity that the norm equals numerator over denominator.
proof idea
Term-mode certificate. Rewrite the target via the identity that the rationalized summand equals its numerator divided by its denominator. Unfold the numerator and denominator definitions together with the Freudenthal squared-edge tuple and the opposite Cayley–Menger vertex map for the given edge. Simplify with the explicit cofactor polynomial and cofactor-partial match tables, then discharge the resulting rational arithmetic by norm_num to obtain $-2$.
why it matters
This is one concrete cell in the $6\times 6$ lookup that the parent theorem freudenthalSchlaefliPolySummandNorm_eq_table assembles by case analysis on edge and coordinate indices. That table is the computational backbone of the Freudenthal length-chain endpoint certificates: it turns the abstract rationalized Schläfli summands into a closed numeric table feeding dihedralClosedDerivLength and thence freudenthalLocalPairClosedFormSchlaefliCoeff.
In the Recognition gravity stack, Freudenthal triangulation of the cube supplies the local discrete geometry on which length-chain and dihedral responses are evaluated. Certifying each summand entry by direct cofactor arithmetic removes floating-point or CAS gaps from that chain. The result is pure Euclidean 3-geometry (no RS constants appear here); its role is to lock the geometric coefficient table that later gravity identities consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.