snorm_zero_0_3
plain-language theorem explainer
For the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand on edge 0 with respect to squared-edge coordinate 3 vanishes. Gravity and discrete-geometry workers cite it when filling the 6×6 Schläfli-norm table at the Freudenthal edge lengths. The proof rewrites the summand as a numerator over denominator, unfolds the Cayley–Menger cofactors, 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 $0$ and squared-edge coordinate $3$ equals $0$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summands on the Freudenthal tetrahedron and the induced closed-form length-derivative table used by local pair coefficients.
A Freudenthal tetrahedron in the unit cube has squared edges $a=(1,2,3,1,2,\ldots)$: three unit steps, two face diagonals, and one body diagonal (freudenthalTetSqEdges). Dihedral data are read from Cayley–Menger cofactors. For each tetrahedral edge $e$, oppositeCMVertices names the two CM vertices opposite that edge; the cofactor polynomials cmCofactor3Poly and their partials cmCofactorPartial are the explicit algebraic normal forms of those minors and derivatives.
The quantity schlaefliPolySummandNorm is the rationalized Schläfli summand: after clearing the arccos radical via the cofactor discriminant, each summand is a pure rational expression in the squared edges (up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}3(a)}$). It is written as numerator over denominator, with denominator $2,C{pp}C_{qq}$ built from the opposite-vertex diagonal cofactors.
proof idea
One short tactic script. Rewrite the target with schlaefliPolySummandNorm_eq_num_div_den so the claim is a ratio of the explicit numerator and denominator. Unfold schlaefliPolySummandNum, schlaefliPolySummandDen, the Freudenthal edge tuple, and oppositeCMVertices (edge $0$ opposite vertices $3,4$). Simplify the resulting cofactor polynomials and partials via cmCofactor3Poly and cmCofactorPartial, then close by norm_num, which evaluates the concrete rationals at $a$ to zero.
why it matters
This is one cell of the Freudenthal Schläfli-norm lookup table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table matches every $(e,k)$ entry of schlaefliPolySummandNorm at the Freudenthal edges against that table by case-splitting; the $(0,3)$ case is discharged exactly by this lemma (siblings cover the other pairs).
Those certified summands feed the closed-form dihedralClosedDerivLength table for freudenthalLocalPairClosedFormSchlaefliCoeff, the local length-chain endpoint data in the gravity layer. In the broader Recognition geometry stack this is discrete differential geometry on the eight-tick / cube triangulation side (Freudenthal decomposition of the unit cube), not a forcing-chain T0–T8 step, but it supplies the algebraic endpoint certificates those gravity identities consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.