snorm_zero_5_2
plain-language theorem explainer
The rationalized Schläfli summand on the Freudenthal tetrahedron vanishes at edge index 5 and squared-edge coordinate 2. Authors of the closed-form dihedral length-chain table cite this as one of the thirty-six cell certificates. The proof rewrites the summand as a cofactor numerator over denominator, unfolds the Freudenthal edge lengths and opposite-vertex map, then finishes by polynomial simplification 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 $5$ and squared-edge coordinate $2$ is zero: $N_{\mathrm{Sch}}(a,5,2)=0$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on the local Freudenthal tetrahedron, and the induced closed-form table for the dihedral length derivative used in gravity length-chain work.
A Freudenthal tetrahedron in the unit cube has squared-edge data $a$ with three unit steps, two face diagonals of square-length 2, and one body diagonal of square-length 3. Dihedral geometry is read from Cayley-Menger cofactors: cmCofactor3Poly is the explicit polynomial normal form of each $5\times 5$ cofactor, and cmCofactorPartial is its partial with respect to one squared-edge coordinate. For each tetrahedral edge $e$, oppositeCMVertices names the two CM vertices opposite that edge.
The rationalized summand schlaefliPolySummandNorm removes the arccos radical via the cofactor discriminant. Up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, it is the pure rational expression whose numerator and denominator are built from those cofactors (and their partials). The identity schlaefliPolySummandNorm_eq_num_div_den records that fraction form.
proof idea
Term-mode certificate, four steps. Rewrite via schlaefliPolySummandNorm_eq_num_div_den so the claim is a ratio of explicit polynomials. Unfold the numerator, the denominator, the Freudenthal squared-edge tuple, and the opposite-vertex pairing for edge 5. Simplify with the match-tables for cmCofactor3Poly and cmCofactorPartial. Close by norm_num, which evaluates the concrete rationals at the Freudenthal lengths to zero.
why it matters
One cell of the $6\times 6$ Freudenthal Schläfli-norm table. Downstream, freudenthalSchlaefliPolySummandNorm_eq_table matches on $(e,k)$ and dispatches each pair to a sibling certificate; the $(5,2)$ arm is exactly this theorem. That table is the algebraic input to the closed-form dihedralClosedDerivLength data for freudenthalLocalPairClosedFormSchlaefliCoeff (module goal).
In the broader RS gravity stack, Freudenthal cube triangulation supplies the discrete 3-space scaffolding on which length-chain and dihedral identities are evaluated. Vanishing cells prune the derivative table and keep the closed form sparse. The result is pure Euclidean 3-geometry (Cayley-Menger / Schläfli); it does not itself invoke the T0-T8 forcing chain, but it is the kind of rigid combinatorial input those continuum limits later consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.