snorm_0_5
plain-language theorem explainer
For the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand at edge 0 with respect to squared-edge coordinate 5 equals 2. Gravity and discrete-geometry workers cite this as one cell of the 6×6 closed-form table. The proof rewrites the summand as a cofactor numerator over denominator, unfolds the Freudenthal edge lengths and opposite-vertex map, then finishes by simp and norm_num.
Claim. Let $a$ be the squared-edge 6-tuple of a Freudenthal tetrahedron in the unit cube ($a=(1,2,3,1,2,3)$ in the standard edge ordering). The rationalized Schläfli summand of $a$ at edge index $e=0$ differentiated in squared-edge coordinate $k=5$ equals $2$.
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 length-derivative table used by local pair coefficients.
A Freudenthal tetrahedron tiles the unit cube; its squared edges are three unit steps, two face diagonals, and one body diagonal, packaged as freudenthalTetSqEdges. Dihedral geometry is read from Cayley–Menger cofactors: cmCofactor3Poly is the explicit polynomial normal form of each $3\times 3$ cofactor, and cmCofactorPartial is its partial in one squared-edge coordinate. For each tetrahedral edge, oppositeCMVertices names the two CM vertices opposite that edge.
The rationalized summand schlaefliPolySummandNorm removes the arccos radical via the cofactor discriminant. Up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, it is the pure rational expression whose numerator and denominator are built from those cofactors (schlaefliPolySummandNum / schlaefliPolySummandDen).
proof idea
One short tactic script. Rewrite via schlaefliPolySummandNorm_eq_num_div_den so the claim is a ratio of the explicit numerator and denominator polynomials. Unfold the numerator, denominator, the Freudenthal squared-edge tuple, and the opposite-vertex pairing for edge 0. Simplify the resulting cofactor polynomials and partials with the match-tables in cmCofactor3Poly and cmCofactorPartial. Close the concrete rational arithmetic by norm_num, obtaining the constant 2.
why it matters
This is one certified cell of the Freudenthal Schläfli-norm lookup table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table matches every $(e,k)$ entry of that table to the evaluated rationalized summand by case-splitting on Fin 6 × Fin 6 and dispatching to the sibling certificates (snorm_0_5 handles $(0,5)$).
Those table values feed the closed-form length derivative dihedralClosedDerivLength and thence freudenthalLocalPairClosedFormSchlaefliCoeff in the gravity length-chain. In the broader Recognition geometry stack, Freudenthal triangulation supplies the discrete 3-space scaffolding consistent with the forced $D=3$ landmark (T8); certified Schläfli coefficients keep the local curvature/dihedral response exact rather than numeric.
No open scaffold remains here: the claim is fully proved and only assembles already-explicit cofactor polynomials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.