snorm_zero_3_5
plain-language theorem explainer
The rationalized Schläfli summand for a Freudenthal tetrahedron vanishes at edge index 3 and squared-edge coordinate 5. Gravity and discrete-geometry workers cite it when filling the 6×6 closed-form table of dihedral length derivatives on the unit-cube triangulation. The proof rewrites the summand as a pure rational expression, unfolds the Cayley–Menger cofactor polynomials at the fixed Freudenthal edge lengths, and evaluates to zero by numeric simplification.
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 tetrahedral edge $e=3$ and squared-edge coordinate $k=5$ equals $0$.
background
The module certifies the full $6\times 6$ table of rationalized Schläfli summands on the Freudenthal tetrahedron, and the induced closed-form length derivatives used by the local pair coefficient in the gravity length chain.
A Freudenthal tetrahedron tiles the unit cube; its squared edges are the fixed tuple freudenthalTetSqEdges: three unit steps, two face diagonals of squared length 2, and one body diagonal of squared length 3. Dihedral angles of a tetrahedron are recovered from Cayley–Menger cofactors. The opposite-vertex map sends each of the six edges to the pair of CM indices opposite that edge.
The rationalized Schläfli summand 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 is the original polynomial-cofactor summand. Its numerator and denominator are built from the explicit cofactor polynomials and their partials with respect to squared-edge coordinates.
proof idea
Rewrite the summand via the identity that equates it to numerator over denominator. Unfold the numerator, the denominator, the Freudenthal squared-edge tuple, and the opposite-vertex pairing for edge 3. Simplify with the explicit match-tables for the degree-3 cofactor polynomial and its partial derivatives. Finish by norm_num, which evaluates the resulting rational expression at the concrete integer edge lengths to 0.
why it matters
This is one cell of the exhaustive $6\times 6$ certificate that the lookup table freudenthalSchlaefliPolySummandNormTable matches the evaluated rationalized summands. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table dispatches on $(e,k)$ and cites this lemma for the pair $(3,5)$.
That table feeds the closed-form dihedralClosedDerivLength data for freudenthalLocalPairClosedFormSchlaefliCoeff, the local geometric coefficient in the Freudenthal length-chain endpoint certification on the gravity side. In the broader Recognition geometry stack it supplies a concrete, machine-checked input to discrete curvature and length-response identities on the eight-tick spatial lattice (T7–T8), without leaving residual radicals in the dihedral derivatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.