snorm_5_1
plain-language theorem explainer
Certifies that the rationalized Schläfli summand on the Freudenthal tetrahedron squared-edge data equals -1 at edge index 5 and squared-edge coordinate 1. Gravity and discrete-geometry workers cite it when assembling the full 6×6 summand table. The proof decomposes the summand into numerator over denominator, unfolds the cofactor polynomials on the fixed edge lengths, and finishes by numeric normalization.
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=5$ and squared-edge coordinate $k=1$ equals $-1$.
background
The module certifies the full $6\times 6$ grid of rationalized Schläfli summands on the local Freudenthal tetrahedron, then the induced closed-form length-derivative table used by the Freudenthal local-pair Schläfli coefficients.
A Freudenthal tetrahedron tiles the unit cube; its squared edges are the fixed tuple $a$ with values $1,2,3,1,2,3$ (unit steps, face diagonals, body diagonal). Dihedral geometry is read from Cayley-Menger cofactors: for each edge $e$, oppositeCMVertices supplies the two CM indices opposite that edge, and cmCofactor3Poly is the explicit polynomial normal form of every $3\times 3$ cofactor in the squared-edge coordinates. Partials cmCofactorPartial differentiate those polynomials in one squared-edge slot.
The Schläfli summand is the cofactor expression that appears in the derivative of a dihedral angle. schlaefliPolySummandNorm is that summand after clearing the arccos radical via the cofactor discriminant: up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, it is a pure rational function of the squared edges, written as numerator over denominator (products of opposite diagonal cofactors).
proof idea
One short computation certificate. Rewrite the target with schlaefliPolySummandNorm_eq_num_div_den so the claim is an equality of an explicit rational expression to $-1$. Unfold the numerator and denominator definitions together with freudenthalTetSqEdges and oppositeCMVertices, which pins every cofactor index and every squared-edge entry to a concrete number. simp reduces cmCofactor3Poly and cmCofactorPartial on those constants; norm_num evaluates the resulting rational arithmetic to $-1$.
why it matters
Fills one cell of the Freudenthal Schläfli summand table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table states that the lookup table matches the evaluated rationalized summands for every $(e,k)\in\mathrm{Fin},6\times\mathrm{Fin},6$, and dispatches the $(5,1)$ case by exact this lemma.
That table is the computational backbone of the module's closed-form dihedralClosedDerivLength data for freudenthalLocalPairClosedFormSchlaefliCoeff. In the gravity chain, those coefficients feed length-endpoint identities on the discrete Freudenthal complex: exact rational summands replace symbolic arccos derivatives, so downstream curvature and deficit identities stay in $\mathbb{Q}$.
The result is pure geometry (Cayley-Menger + Schläfli on a fixed tet), not a forcing-chain step, but it is the kind of machine-checked local identity the RS gravity layer needs before global continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.