snorm_4_0
plain-language theorem explainer
On the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand for edge index 4 and squared-edge coordinate 0 equals −2. Gravity and discrete-geometry proofs cite it when assembling the full 6×6 summand table. The proof rewrites the summand as a numerator/denominator ratio, unfolds the Cayley–Menger cofactor polynomials at the fixed edge lengths, and finishes by numeric normalization.
Claim. For the Freudenthal tetrahedron squared-edge tuple (three unit edges, two face diagonals, one body diagonal), the rationalized Schläfli summand at edge $e=4$ and coordinate $k=0$ equals $-2$.
background
The module certifies every entry of the $6\times 6$ evaluation of the rationalized Schläfli summand on the local Freudenthal tetrahedron, and the induced closed-form length-derivative table used by freudenthalLocalPairClosedFormSchlaefliCoeff.
A Freudenthal tetrahedron tiles the unit cube; its squared-edge 6-tuple is fixed: three edges of length squared $1$, two face diagonals of length squared $2$, and one body diagonal of length squared $3$. The Schläfli identity for a tetrahedron expresses dihedral-angle derivatives in terms of Cayley–Menger cofactors of that edge tuple. The rationalized summand schlaefliPolySummandNorm removes the arccos radical by clearing the cofactor discriminant, leaving a pure rational expression in the six squared edges.
Numerator and denominator are built from the explicit cofactor polynomials cmCofactor3Poly and their partials cmCofactorPartial, indexed by the pair of Cayley–Menger vertices opposite the chosen edge (oppositeCMVertices).
proof idea
Rewrite the summand via schlaefliPolySummandNorm_eq_num_div_den into an explicit numerator over denominator. Unfold the numerator, denominator, the fixed Freudenthal edge tuple, and the opposite-vertex map for edge 4. Simplify the resulting cofactor polynomials and partials with the match-based definitions of cmCofactor3Poly and cmCofactorPartial. Close by norm_num, which evaluates the concrete rational expression to $-2$.
why it matters
One cell of the complete $6\times 6$ certificate table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table dispatches on $(e,k)$ and cites this lemma for the $(4,0)$ case, proving the lookup table matches the evaluated rationalized summands. That table feeds the closed-form length-chain derivative used in the discrete gravity / Freudenthal length-chain endpoint certificates. In the broader Recognition geometry stack this is pure Euclidean bookkeeping: it supplies the numerical Schläfli coefficients on the canonical cube triangulation that underpins continuum limits and curvature identities, without invoking the forcing chain (T0–T8) or the Recognition Composition Law directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.