snorm_4_3
plain-language theorem explainer
At the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand for edge index 4 and squared-edge coordinate 3 equals −4. Gravity and discrete-geometry workers cite this as one cell of the closed 6×6 certificate table. 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 $\mathrm{snorm}(a; e, k)$ at edge $e=4$ and coordinate $k=3$ equals $-4$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on the Freudenthal tetrahedron, feeding a closed-form table for the local dihedral length derivative used in the gravity length-chain.
A Freudenthal tetrahedron tiles the unit cube; its squared edges are fixed as $a=(1,2,3,1,2,\ldots)$ (unit steps, face diagonals, body diagonal). The Schläfli identity differentiates dihedral angles against edge lengths. After clearing the arccos radical via the Cayley–Menger cofactor discriminant, each summand becomes a pure rational function of the squared edges: numerator built from cofactors and their partials, denominator $2,C_{pp}C_{qq}$ for the pair of vertices opposite the chosen edge.
Upstream, cmCofactor3Poly and cmCofactorPartial supply the explicit polynomial normal forms; oppositeCMVertices names the opposite pair for each of the six edges; schlaefliPolySummandNorm_eq_num_div_den identifies the summand with that fraction.
proof idea
One short tactic script. Rewrite the summand via the numerator/denominator identity. Unfold the numerator and denominator definitions together with the Freudenthal squared-edge tuple and the opposite-vertex lookup for edge 4. Simplify the resulting cofactor polynomials and partial derivatives by their match clauses, then discharge the concrete rational arithmetic with norm_num to obtain $-4$.
why it matters
This is one concrete cell of the Freudenthal Schläfli-norm table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table matches every $(e,k)$ entry by case-splitting onto lemmas of this family, so the closed-form coefficient table for freudenthalLocalPairClosedFormSchlaefliCoeff is fully certified rather than assumed.
In the Recognition gravity stack the length-chain endpoint needs these numerical Schläfli weights on the discrete tetrahedral mesh; without the evaluated rationals the dihedral closed derivative stays symbolic. The result is pure 3D Cayley–Menger algebra (consistent with the forced $D=3$ landmark) and does not itself invoke the J-cost or $\varphi$-ladder, but it locks a geometric input those layers consume downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.