snorm_zero_4_5
plain-language theorem explainer
For the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand at edge pair (4,5) vanishes. Gravity and discrete-geometry workers cite it when assembling the 6×6 closed-form coefficient table for local dihedral length derivatives. The proof rewrites the summand as a pure rational expression, unfolds the Cayley–Menger cofactor polynomials on the fixed squared-edge tuple, and finishes by numeric simplification to zero.
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 $\mathrm{snorm}(a; e, k)$, obtained from the Cayley–Menger cofactor polynomials after clearing the arccos radical, satisfies $\mathrm{snorm}(a; 4, 5) = 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 local dihedral length derivatives. A Freudenthal tetrahedron tiles the unit cube; its squared edges are the fixed tuple with values $1,2,3,1,2$ on the first five slots (unit steps, face diagonals) and the body diagonal on the last.
The Schläfli identity expresses dihedral-angle variation in terms of edge lengths. After Cayley–Menger cofactors remove the arccos radical, each summand becomes a pure rational function of the six squared edges: numerator built from a cofactor and its partials, denominator twice the product of the two opposite principal cofactors. Upstream, cmCofactor3Poly is the explicit polynomial normal form of every $3\times 3$ cofactor, and cmCofactorPartial is its partial with respect to one squared-edge coordinate. Opposite vertex pairs for each edge are given by the standard Cayley–Menger indexing.
proof idea
One short computational certificate. Rewrite the rationalized summand via the identity that splits it into numerator over denominator. Unfold the numerator and denominator definitions together with the Freudenthal squared-edge tuple and the opposite-vertex map for the edge indices. The resulting expression is a combination of the explicit cofactor polynomials and their partials; simp reduces those match-expressions on the concrete indices, and norm_num evaluates the rational number to zero.
why it matters
This is one cell of the exhaustive $6\times 6$ certificate table for Freudenthal Schläfli summands. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table dispatches on $(e,k)$ and quotes each cell lemma (including this one) to prove that the evaluated rationalized summands equal the stored lookup table. That table feeds the closed-form coefficients of the local dihedral length derivative used in the gravity length-chain endpoint analysis.
In the broader Recognition geometry stack, Freudenthal triangulation supplies the discrete 3-space scaffolding compatible with the forced $D=3$ and eight-tick octave landmarks; vanishing and nonzero summand entries determine which edge-length variations couple into dihedral response. The result is pure geometry: no open hypothesis remains for this cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.