snorm_5_0
plain-language theorem explainer
At the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand for edge index 5 and squared-edge coordinate 0 equals 2. Gravity and discrete-geometry proofs cite this as one cell of the 6×6 closed-form table. The proof rewrites the summand as a numerator/denominator of Cayley–Menger cofactors, unfolds 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 $e=5$ and squared-edge coordinate $k=0$ equals $2$.
background
The module certifies a full $6\times 6$ evaluation of the rationalized Schläfli summand on the Freudenthal tetrahedron, feeding a closed-form table for local dihedral length derivatives.
A Freudenthal tetrahedron in the unit cube has fixed squared edges $a=(1,2,3,1,2,3)$: three unit steps, two face diagonals, and one body diagonal. 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 schlaefliPolySummandNorm of the squared edges.
That rational form is a ratio of explicit cofactor polynomials and their partials: opposite Cayley–Menger vertices for each edge determine the denominator $2,C_{pp}C_{qq}$, while the numerator mixes off-diagonal cofactors and $\partial C/\partial a_k$. Upstream, cmCofactor3Poly and cmCofactorPartial supply the expanded polynomials, and oppositeCMVertices labels the pair opposite each of the six edges.
proof idea
One short computational certificate. Rewrite the summand via schlaefliPolySummandNorm_eq_num_div_den as numerator over denominator. Unfold the numerator and denominator definitions together with freudenthalTetSqEdges and oppositeCMVertices for $(e,k)=(5,0)$, so every cofactor index becomes concrete. simp expands cmCofactor3Poly and cmCofactorPartial at those indices on the fixed edge tuple; norm_num evaluates the resulting rational expression to $2$.
why it matters
This is one of the thirty-six atomic cells that assemble freudenthalSchlaefliPolySummandNorm_eq_table, which asserts the lookup table equals the evaluated rationalized summands for every $(e,k)$. That table is the algebraic backbone of the Freudenthal length-chain endpoint certificates and the induced closed-form dihedralClosedDerivLength data used by freudenthalLocalPairClosedFormSchlaefliCoeff.
In the gravity stack, Freudenthal triangulation of the cube is the discrete geometric substrate for local length-chain identities. Pinning each Schläfli summand to an exact rational removes symbolic radicals from dihedral derivatives and lets downstream gravity lemmas quote a constant rather than re-expand cofactors. The result is pure 3D Euclidean tetrahedron algebra (consistent with the framework’s $D=3$ landmark) and does not itself invoke Recognition forcing or constants; it supplies geometry infrastructure those layers consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.