snorm_zero_2_5
plain-language theorem explainer
For the Freudenthal unit-cube tetrahedron edge lengths, the rationalized Schläfli summand at edge index 2 and squared-edge coordinate 5 vanishes. Gravity and discrete-geometry workers cite this as one cell of the 6×6 certificate table that feeds the closed-form dihedral length derivative. The proof is a short unfold-and-norm_num evaluation of the cofactor polynomials.
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 $\mathrm{snorm}(a;e,k)$ at edge $e=2$ and coordinate $k=5$ equals $0$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on the Freudenthal tetrahedron and the induced closed-form table for the local pair Schläfli coefficient used in length-chain gravity.
A Freudenthal tetrahedron tiles the unit cube; its squared edges are fixed as $a=(1,2,3,1,2,3)$ (three unit steps, two face diagonals, one body diagonal). The Schläfli identity expresses the differential of solid angle in terms of dihedral angles; after Cayley–Menger cofactors remove the arccos radical, each summand becomes a pure rational function schlaefliPolySummandNorm of the six squared edges.
That rational form is numerator over denominator built from opposite-vertex cofactors (cmCofactor3Poly) and their partials (cmCofactorPartial). The opposite Cayley–Menger vertex pair for each tetrahedral edge is given by oppositeCMVertices. Upstream, schlaefliPolySummandNorm_eq_num_div_den identifies the summand with that explicit fraction.
proof idea
Rewrite the summand via schlaefliPolySummandNorm_eq_num_div_den as numerator over denominator. Unfold the numerator, denominator, the Freudenthal edge tuple, and the opposite-vertex map. Simplify the resulting cofactor polynomials and partials with the explicit match clauses of cmCofactor3Poly and cmCofactorPartial. Finish by norm_num, which evaluates the concrete rational expression at the numeric Freudenthal edges to zero.
why it matters
This is one cell of the exhaustive $6\times 6$ certificate grid. Downstream, freudenthalSchlaefliPolySummandNorm_eq_table matches every summand against a lookup table by casing on $(e,k)$ and invoking the corresponding snorm_* lemma (including this one for $(2,5)$). That table supplies the closed-form dihedralClosedDerivLength data for freudenthalLocalPairClosedFormSchlaefliCoeff, the length-chain endpoint used in the discrete gravity sector. The certificates turn the abstract Schläfli–Cayley–Menger calculus into concrete numbers on the Freudenthal lattice, which is the geometric substrate for Recognition Science length and curvature bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.