snorm_2_1
plain-language theorem explainer
The rationalized Schläfli summand on the Freudenthal tetrahedron, at edge index 2 and squared-edge coordinate 1, equals -3. Gravity and discrete-geometry workers cite it when filling the 6 imes6 certificate table that drives the closed-form dihedral length derivative. The proof rewrites the summand as numerator over denominator, unfolds the Cayley-Menger cofactor polynomials at the Freudenthal edge lengths, and finishes by numeric simplification.
Claim. Let $a$ be the Freudenthal local squared-edge tuple (three unit steps, two face diagonals, one body diagonal). The rationalized Schläfli summand of $a$ at edge index $2$ and squared-edge coordinate $1$ equals $-3$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on every Freudenthal tetrahedron in the unit cube, and the induced closed-form table for the local-pair Schläfli coefficient.
A Freudenthal tetrahedron has squared edges $a=(1,2,3,1,2,3)$: three unit steps, two face diagonals, and one body diagonal. The Schläfli identity expresses dihedral-angle derivatives in terms of Cayley-Menger cofactors of those edges. The rationalized summand removes the arccos radical via the cofactor discriminant, leaving a pure rational expression (numerator over a product of two diagonal cofactors) up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$.
Opposite Cayley-Menger vertices for each tetrahedral edge select which cofactor pair enters the denominator. Explicit polynomial normal forms and their partials in the squared-edge coordinates make the evaluation fully algebraic.
proof idea
Rewrite the summand via the identity that equates it to numerator over denominator. Unfold the numerator, the denominator, the Freudenthal squared-edge tuple, and the opposite-vertex map for edge 2. Simplify with the explicit cofactor polynomial and cofactor-partial match tables. Close by norm_num, which evaluates the resulting rational expression to $-3$.
why it matters
This is one cell of the $6\times 6$ certificate grid. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table matches every evaluated summand against a lookup table by case-splitting on $(e,k)$ and dispatching to these unit certificates; the $(2,1)$ case lands here.
That table feeds the closed-form dihedral length-derivative coefficients for the Freudenthal local pair, the geometric backbone of the length-chain gravity certificates in this module. In the broader Recognition framework the Freudenthal triangulation supplies the discrete 3-space scaffolding consistent with the forced $D=3$ step of the forcing chain; certified Schläfli summands keep the dihedral calculus exact rather than numeric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.