snorm_2_2
plain-language theorem explainer
For the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand at edge index 2 and squared-edge coordinate 2 equals 2. Gravity and discrete-geometry workers cite it when assembling the 6×6 closed-form coefficient table for local dihedral derivatives. The proof rewrites the summand as a cofactor numerator over denominator, unfolds the Freudenthal edge tuple and opposite-vertex map, then finishes by simp and norm_num.
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=2$ and squared-edge coordinate $k=2$ 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 local pair dihedral derivatives used in the length-chain gravity pipeline.
A Freudenthal tetrahedron tiles the unit cube; its squared-edge tuple freudenthalTetSqEdges is three unit steps, two face diagonals, and one body diagonal. The Schläfli identity expresses the differential of solid angle in terms of edge-length derivatives and dihedral angles. After clearing the arccos radical via the Cayley-Menger cofactor discriminant, each summand becomes the pure rational schlaefliPolySummandNorm.
That norm is a ratio of cofactor polynomials: numerator built from partials of the $3\times 3$ Cayley-Menger cofactors, denominator $2,C_{pp}C_{qq}$ where $(p,q)$ are the two CM vertices opposite the chosen edge (oppositeCMVertices). Explicit polynomial forms are cmCofactor3Poly and cmCofactorPartial.
proof idea
One short computational certificate. Rewrite via schlaefliPolySummandNorm_eq_num_div_den so the goal is numerator over denominator. Unfold the numerator and denominator definitions together with the Freudenthal squared-edge tuple and the opposite-vertex pairing for edge 2. Simplify with the explicit match clauses of cmCofactor3Poly and cmCofactorPartial, then close the resulting rational arithmetic by norm_num, obtaining the constant 2.
why it matters
This is one cell of the exhaustive $6\times 6$ lookup that the parent theorem freudenthalSchlaefliPolySummandNorm_eq_table assembles by case analysis on $(e,k)$. That table is the concrete coefficient source for freudenthalLocalPairClosedFormSchlaefliCoeff and the closed-form length-chain dihedral derivative used in the Gravity domain.
In the broader Recognition geometry stack the Freudenthal triangulation supplies the discrete 3-space scaffolding consistent with the T8 forcing of $D=3$ and the eight-tick octave; certified Schläfli coefficients keep the continuum limit of the length chain free of floating-point or radical branches. The result is fully proved (no sorry), so it closes rather than opens a scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.