snorm_zero_1_0
plain-language theorem explainer
The rationalized Schläfli summand on the Freudenthal tetrahedron vanishes at edge index 1 and squared-edge coordinate 0. Discrete-geometry and gravity workers cite it when filling the closed-form 6×6 dihedral length-chain table. The proof rewrites the summand as a cofactor numerator over denominator, unfolds the Freudenthal edge data and opposite-vertex map, then discharges 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 $N(a,e,k)$ at edge $e=1$ and coordinate $k=0$ satisfies $N(a,1,0)=0$.
background
The module certifies a full $6\times 6$ evaluation of the rationalized Schläfli summand on the local Freudenthal tetrahedron, and the induced closed-form table for the dihedral length-chain coefficient. Freudenthal triangulation chops the unit cube into congruent tetrahedra whose squared edges are fixed: three unit steps, two face diagonals of length $\sqrt{2}$, and one body diagonal of length $\sqrt{3}$ (encoded as freudenthalTetSqEdges).
Schläfli identity relates volume change of a tetrahedron to edge-length derivatives of dihedral angles. After Cayley–Menger cofactors remove the arccos radical, each summand becomes a pure rational expression schlaefliPolySummandNorm: numerator built from a $3\times 3$ cofactor and its partial in one squared-edge coordinate, denominator the product of the two opposite-vertex diagonal cofactors. Opposite vertices for each of the six edges are given by oppositeCMVertices. Explicit polynomial normal forms for those cofactors and partials live in cmCofactor3Poly and cmCofactorPartial.
proof idea
One short evaluation script. Rewrite via schlaefliPolySummandNorm_eq_num_div_den so the claim is a ratio of the explicit numerator and denominator. Unfold the numerator, denominator, the Freudenthal squared-edge assignment, and the opposite-vertex pairing for edge 1. Simplify with the match-tables for cmCofactor3Poly and cmCofactorPartial; the resulting rational expression is identically zero, finished by norm_num.
why it matters
This is one certified cell of the Freudenthal Schläfli norm table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table dispatches on $(e,k)$ and invokes this lemma for the $(1,0)$ case, so the lookup table matches the evaluated rationalized summands. That table feeds the closed-form dihedralClosedDerivLength data used by freudenthalLocalPairClosedFormSchlaefliCoeff in the gravity length-chain endpoint certificates.
In the broader Recognition geometry stack, Freudenthal cube triangulation supplies the discrete 3-space scaffolding consistent with the forced $D=3$ landmark (T8). Exact vanishing of selected Schläfli summands simplifies the length-chain derivatives that later couple to the recognition cost and mass ladder; without these zero certificates the closed-form gravity table would remain symbolic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.