snorm_zero_0_1
plain-language theorem explainer
For the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand at edge 0 differentiated in squared-edge coordinate 1 vanishes. Gravity and discrete-geometry workers cite it when filling the 6×6 summand table that feeds the closed-form dihedral length derivative. The proof rewrites the summand as a numerator over denominator, unfolds the Cayley–Menger cofactors on the fixed edge lengths, and finishes 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 edge index $0$ with respect to squared-edge coordinate $1$ 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-pair Schläfli coefficient used in length-chain gravity.
A Freudenthal tetrahedron in the unit cube has fixed squared edges $a=(1,2,3,1,2,\ldots)$: 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 Cayley–Menger cofactors; up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, it equals the original polynomial-cofactor summand. Its denominator is twice the product of the two opposite diagonal cofactors, and its numerator is built from those cofactors and their partials in the squared-edge coordinates.
Opposite Cayley–Menger vertices for each tetrahedral edge, together with the explicit cofactor polynomials and their partial derivatives, supply the algebraic raw material for every entry of the table.
proof idea
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 $0$. Simplify with the explicit Cayley–Menger cofactor polynomial and its partials; norm_num then shows the resulting rational expression is zero.
why it matters
This is one cell of the $6\times 6$ certificate table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table matches every evaluated rationalized summand against a lookup table by case-splitting on $(e,k)$ and invoking the corresponding snorm_* lemma; the $(0,1)$ case is discharged exactly here.
That table induces the closed-form dihedralClosedDerivLength data for freudenthalLocalPairClosedFormSchlaefliCoeff, which is the discrete-geometry input to the Freudenthal length-chain side of the gravity development. In the broader Recognition framework the construction sits in the geometric scaffolding that supports continuum limits and curvature bookkeeping on the eight-tick, $D=3$ lattice forced by T7–T8; it does not itself invoke the J-cost or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.