snorm_1_1
plain-language theorem explainer
The rationalized Schläfli summand on the Freudenthal tetrahedron squared-edge data equals 2 at edge index 1 and squared-edge coordinate 1. Authors of the closed-form dihedral length-chain table cite this cell certificate. The proof rewrites the summand as numerator over denominator, unfolds the Cayley-Menger cofactors for those opposite vertices, and finishes by numeric simplification.
Claim. Let $a$ be the Freudenthal local squared-edge 6-tuple (three unit edges, two face diagonals of squared length 2, one body diagonal of squared length 3). The rationalized Schläfli summand of $a$ at tetrahedral edge index $1$ and squared-edge coordinate index $1$ equals $2$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on the Freudenthal tetrahedron, and the induced closed-form table for the local-pair Schläfli coefficient used in the length-chain derivative.
A Freudenthal tetrahedron in the unit cube has squared edges $a=(1,2,3,1,2,3)$: three unit steps, two face diagonals, one body diagonal. The Schläfli identity for a tetrahedron expresses the differential of solid angle in terms of dihedral angles; after Cayley-Menger elimination of the arccos radical, each summand becomes a pure rational function of the squared edges.
That rationalized summand is built from opposite Cayley-Menger vertex pairs for the chosen edge and from the explicit cofactor polynomials (and their partials) in the six squared-edge coordinates. The denominator is twice the product of the two diagonal cofactors at those opposite vertices; the numerator is the corresponding cofactor data after differentiation in one edge coordinate.
proof idea
One short algebraic evaluation. Rewrite the summand via the identity that it equals numerator over denominator. Unfold the numerator and denominator definitions together with the Freudenthal edge tuple and the opposite-vertex map for edge 1. Simplify the resulting cofactor polynomials and their partials by the explicit match tables, then close with norm_num to obtain the constant 2.
why it matters
This is one cell of the $6\times 6$ certificate table that discharges freudenthalSchlaefliPolySummandNorm_eq_table, whose doc-comment states that the lookup table matches the evaluated rationalized Schläfli summands. That table is the computational backbone for the closed-form dihedralClosedDerivLength data feeding freudenthalLocalPairClosedFormSchlaefliCoeff.
In the Recognition gravity stack, Freudenthal triangulation of the cube supplies the discrete length chain on which continuum curvature and Newtonian limits are read off. Exact rational values of the Schläfli summands remove floating-point and radical obstacles from those length derivatives. The result is pure geometry infrastructure; it does not itself invoke the forcing chain (T0-T8) or the Recognition Composition Law, but it is a necessary certified input to the gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.