snorm_zero_5_3
plain-language theorem explainer
The rationalized Schläfli summand for the Freudenthal unit-cube tetrahedron vanishes at edge index 5 and squared-edge coordinate 3. Discrete-geometry and RS gravity workers cite it as one cell of the closed 6×6 certificate table. Proof rewrites the summand as a cofactor numerator over denominator, unfolds the fixed Freudenthal edge lengths, and finishes by numeric simplification.
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 $3$ equals $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 length-derivative table used by the Freudenthal length-chain.
A Freudenthal tetrahedron tiles the unit cube; its squared edges are the fixed tuple $a=(1,2,3,1,2,\ldots)$ (unit steps, face diagonals, body diagonal). Dihedral geometry is encoded via Cayley-Menger cofactors: cmCofactor3Poly is the explicit polynomial normal form of each $5\times 5$ cofactor, and cmCofactorPartial is its partial in one squared-edge coordinate. For each tetrahedral edge $e$, oppositeCMVertices names the two CM vertices opposite that edge.
The rationalized Schläfli summand schlaefliPolySummandNorm removes the arccos radical by 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).
proof idea
Rewrite the summand via the identity that it equals numerator over denominator. Unfold the numerator, denominator, the fixed Freudenthal squared-edge tuple, and the opposite-vertex map for edge 5. Simplify with the explicit cofactor polynomial and cofactor-partial match tables, then discharge the resulting rational arithmetic by norm_num, obtaining $0$.
why it matters
This is one cell of the exhaustive $6\times 6$ certificate grid. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table matches every evaluated summand against a lookup table by casing on $(e,k)$ and invoking the corresponding snorm_* lemma; the present result handles the $(5,3)$ case (and records that it is zero).
That table feeds the closed-form dihedralClosedDerivLength data for freudenthalLocalPairClosedFormSchlaefliCoeff, which is the local geometric input to the Freudenthal length-chain in the RS gravity stack. The chain sits in the discrete 3-space geometry forced by T8 ($D=3$) and the eight-tick octave (T7), where tetrahedron dihedral derivatives control length-response of the recognition lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.