snorm_zero_2_0
plain-language theorem explainer
The rationalized Schläfli summand on the Freudenthal unit-cube tetrahedron vanishes at edge index 2 and squared-edge coordinate 0. Discrete-geometry and RS gravity workers cite it when filling the closed-form dihedral length-chain table. Proof rewrites the summand as a cofactor numerator over denominator, unfolds the Freudenthal edges and opposite vertices, then finishes by numeric simplification.
Claim. Let $a_F$ be the squared-edge 6-tuple of a Freudenthal tetrahedron in the unit cube (three edges of squared length $1$, two of $2$, one of $3$). The rationalized Schläfli summand of $a_F$ at tetrahedral edge $e=2$ with respect to squared-edge coordinate $k=0$ equals zero.
background
This module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on the Freudenthal tetrahedron, and the induced closed-form table of dihedral length derivatives used by the local-pair Schläfli coefficient.
A Freudenthal tetrahedron tiles the unit cube. Its squared edges are three unit steps, two face diagonals, and one body diagonal, packaged as the fixed 6-tuple $a_F$ with values $(1,2,3,1,2,3)$ in edge order. Dihedral geometry is handled via Cayley-Menger cofactors: for each edge $e$, oppositeCMVertices returns the two CM vertex indices opposite that edge; cmCofactor3Poly is the explicit polynomial for each cofactor entry, and cmCofactorPartial its partial in one squared-edge coordinate.
The quantity at issue is the rationalized Schläfli summand: after clearing the arccos radical with the cofactor discriminant, each summand is a pure rational expression (numerator from cofactors and partials, denominator $2PQ$ from the two opposite self-cofactors). Up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, this is the original polynomial-cofactor summand.
proof idea
One short computational certificate. Rewrite the summand via the identity that equates it to numerator over denominator. Unfold the numerator and denominator definitions, the Freudenthal squared-edge tuple, and oppositeCMVertices (edge $2$ maps to opposite vertices $(2,3)$). Simplify the resulting expression against the explicit match-tables for cmCofactor3Poly and cmCofactorPartial. The rational number collapses to $0$ by norm_num.
why it matters
Feeds the parent theorem freudenthalSchlaefliPolySummandNorm_eq_table, whose doc-comment states that "the lookup table matches the evaluated rationalized Schläfli summands." That theorem matches on $(e,k)$ and dispatches the $(2,0)$ cell to this result. The table in turn supplies the closed-form dihedral length-derivative data behind freudenthalLocalPairClosedFormSchlaefliCoeff in the gravity length-chain.
In the Recognition framework the Freudenthal triangulation is the discrete spatial scaffold for local geometry (aligned with the forcing-chain step that fixes $D=3$). Pinning every rationalized summand cell, including the zeros, makes the length-chain endpoint certificates fully computational rather than schematic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.