snorm_zero_0_2
plain-language theorem explainer
The rationalized Schläfli summand for the Freudenthal unit-cube tetrahedron vanishes at edge index 0 and squared-edge coordinate 2. Discrete-geometry and RS gravity workers cite it as one cell of the certified 6×6 summand table. The proof rewrites the summand as a cofactor numerator over denominator, unfolds the fixed Freudenthal edge lengths, and closes 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 $N(a;e,k)$ at edge $e=0$ and squared-edge coordinate $k=2$ satisfies $N(a;0,2)=0$.
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 gravity length chain.
A Freudenthal tetrahedron in the unit cube has fixed squared edges $a$: three unit steps, two face diagonals of squared length 2, and one body diagonal of squared length 3 (freudenthalTetSqEdges). Dihedral geometry is packaged via Cayley–Menger cofactors: cmCofactor3Poly is the explicit polynomial normal form of each $5\times 5$ cofactor, and cmCofactorPartial its partial in one squared-edge coordinate. For each tetrahedral edge $e$, oppositeCMVertices names the two CM vertices opposite that edge.
The object being evaluated is schlaefliPolySummandNorm: the Schläfli summand after clearing the arccos radical by the cofactor discriminant, leaving a pure rational expression (numerator over a product of opposite diagonal cofactors). Upstream, schlaefliPolySummandNorm_eq_num_div_den identifies that rational form with the explicit num/den pair.
proof idea
Term-mode computation, not a conceptual argument. Rewrite the summand via schlaefliPolySummandNorm_eq_num_div_den as numerator over denominator. Unfold the numerator, denominator, the fixed Freudenthal squared-edge tuple, and the opposite-vertex map for edge 0. Simplify the resulting cofactor polynomials and partials with the explicit match clauses of cmCofactor3Poly and cmCofactorPartial, then finish by norm_num, which reduces the concrete rational to 0.
why it matters
One cell of the certified lookup table for rationalized Schläfli summands on the Freudenthal tetrahedron. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table dispatches on $(e,k)$ and quotes this lemma for the $(0,2)$ case, so the table entry is definitionally the evaluated summand.
That table feeds the closed-form dihedralClosedDerivLength data behind freudenthalLocalPairClosedFormSchlaefliCoeff in the gravity length-chain endpoint certificates. In the RS geometry stack, Freudenthal triangulation of the cube is the discrete carrier for local length variation; vanishing summands prune the derivative table and simplify the chain endpoint identities. No forcing-chain (T0–T8) step is discharged here; the result is pure computational geometry support for the gravity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.