snorm_1_5
plain-language theorem explainer
At the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand for edge index 1 and squared-edge coordinate 5 equals −2. Gravity and discrete-geometry proofs cite this as one cell of the closed 6×6 evaluation 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 $\mathrm{snorm}(a; e, k)$ at edge $e=1$ and coordinate $k=5$ satisfies $\mathrm{snorm}(a; 1, 5) = -2$.
background
The module certifies the full $6 \times 6$ evaluation of the rationalized Schläfli summand on the local Freudenthal tetrahedron, feeding a closed-form table for the length-chain dihedral derivative.
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 the derivative of a dihedral angle in terms of Cayley–Menger cofactors of those squared edges. After clearing the arccos radical via the cofactor discriminant, each summand becomes a pure rational function schlaefliPolySummandNorm of the six squared lengths.
Upstream, cmCofactor3Poly is the explicit polynomial normal form of every $3 \times 3$ Cayley–Menger cofactor, and cmCofactorPartial is its partial with respect to one squared-edge coordinate. Opposite vertex pairs for each edge come from oppositeCMVertices. The identity schlaefliPolySummandNorm_eq_num_div_den writes the summand as numerator over denominator built from those cofactors.
proof idea
Term-mode certificate by direct evaluation. Rewrite via schlaefliPolySummandNorm_eq_num_div_den so the claim is a ratio of the explicit numerator and denominator polynomials. Unfold the numerator, denominator, the fixed Freudenthal edge tuple, and the opposite-vertex map for edge 1. Simplify with the match-tables for cmCofactor3Poly and cmCofactorPartial, then close with norm_num to obtain the constant $-2$.
why it matters
One cell of the $6 \times 6$ Freudenthal Schläfli-summand table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table dispatches on $(e,k)$ and cites this lemma for the $(1,5)$ case, proving the lookup table matches the evaluated rationalized summands. That table induces the closed-form dihedralClosedDerivLength coefficients used by freudenthalLocalPairClosedFormSchlaefliCoeff in the gravity length-chain endpoint certificates.
In the broader Recognition geometry stack, Freudenthal triangulation of the cube is the discrete scaffold for local curvature and dihedral bookkeeping; certified constant summands remove symbolic cofactor work from every downstream length-chain identity. No forcing-chain (T0–T8) step is touched directly; the result is pure discrete differential geometry supporting the gravity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.