snorm_0_4
plain-language theorem explainer
At the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand for edge 0 and squared-edge coordinate 4 equals −1. Geometry and gravity workers cite this cell when filling the 6×6 certificate table that drives closed-form dihedral length derivatives. The proof rewrites the summand as a cofactor numerator over denominator, 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=0$ and squared-edge coordinate $k=4$ equals $-1$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on the Freudenthal tetrahedron, then the induced closed-form table for local dihedral length derivatives used in the gravity length-chain.
A Freudenthal tetrahedron tiles the unit cube; its squared edges are the fixed tuple $a$ with three unit steps, two face diagonals, and one body diagonal. The Schläfli identity 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 of the squared edges: numerator and denominator built from $3\times 3$ cofactor polynomials and their partials with respect to one squared-edge coordinate. Opposite Cayley–Menger vertex pairs label which cofactors sit on each tetrahedral edge.
Upstream, schlaefliPolySummandNorm is that rational expression (up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$). The equality-to-num/den lemma and the explicit cofactor and partial polynomials are the computational substrate for every cell of the table.
proof idea
One short tactic script. Rewrite the summand via the num/den identity, then unfold the numerator, denominator, the fixed Freudenthal squared-edge tuple, and the opposite-vertex map for edge 0. Simplify with the explicit Cayley–Menger cofactor polynomial and its partials; norm_num evaluates the resulting rational number to $-1$.
why it matters
This is one concrete cell of the $6\times 6$ Freudenthal Schläfli-norm table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table matches every $(e,k)$ entry by case-splitting and invoking the corresponding snorm_* lemma; the $(0,4)$ case is discharged by this result. That table feeds the closed-form coefficient list for freudenthalLocalPairClosedFormSchlaefliCoeff and the dihedral length-derivative certificates in the gravity length-chain.
In the broader Recognition geometry stack, Freudenthal triangulation supplies the discrete 3-space scaffolding (aligned with the forced $D=3$ landmark). Certified rational Schläfli summands turn local edge-length variation into exact algebraic data rather than floating-point dihedral numerics, which is what the length-chain endpoint certificates need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.