snorm_zero_5_5
plain-language theorem explainer
The rationalized Schläfli summand for the Freudenthal unit-cube tetrahedron vanishes at edge index 5 and squared-edge coordinate 5. 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 cofactor numerator over denominator, unfolds the Freudenthal edge lengths and opposite-vertex map, then finishes by simplification and numeric normalization.
Claim. For the Freudenthal tetrahedron squared-edge data (three unit edges, two face diagonals, one body diagonal), the rationalized Schläfli summand at edge $e=5$ and squared-edge coordinate $k=5$ equals $0$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summands on the local Freudenthal tetrahedron inside the unit cube, and the induced closed-form table of dihedral length-derivative coefficients.
A Freudenthal tetrahedron has squared-edge tuple with values $1,2,3,1,2$ on the six edges (unit steps, face diagonals, body diagonal). The Schläfli identity for a tetrahedron expands the derivative of dihedral angle with respect to edge length into cofactor expressions of the Cayley–Menger matrix. After clearing the arccos radical via the cofactor discriminant, each summand becomes a pure rational function schlaefliPolySummandNorm: numerator built from a $3\times 3$ cofactor and its partial in one squared-edge coordinate, denominator twice the product of the two opposite principal cofactors.
Opposite Cayley–Menger vertex pairs for each edge are given by a fixed lookup; cofactors and their partials are the explicit multilinear polynomials cmCofactor3Poly and cmCofactorPartial.
proof idea
Term-mode certificate. Rewrite the summand via the identity that expresses the rationalized norm as numerator over denominator. Unfold the numerator and denominator definitions together with the Freudenthal squared-edge assignment and the opposite-vertex map for edge 5. Simplify the resulting cofactor polynomials and their partials by the explicit match clauses, then discharge the concrete rational arithmetic with norm_num, obtaining zero.
why it matters
One cell of the exhaustive $6\times 6$ certificate grid that proves the lookup table equals the evaluated rationalized Schläfli summands on Freudenthal edges. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table pattern-matches on $(e,k)$ and invokes this lemma for the $(5,5)$ case; that table in turn supplies the closed-form coefficients for local pair dihedral length derivatives used in the gravity length-chain endpoint analysis. In the broader Recognition geometry stack this is pure discrete differential geometry on the cube triangulation (no direct appeal to T0–T8 or the J-cost), but it is required scaffolding for any continuum limit that extracts curvature or length response from the Freudenthal mesh.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.