snorm_1_2
plain-language theorem explainer
For the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand at edge pair (1,2) equals -2. Gravity and discrete-geometry workers cite this when assembling the closed-form dihedral length-derivative table. The proof rewrites the summand as a cofactor numerator over denominator, unfolds the fixed squared-edge data, 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 $N(a;e,k)$ at edge indices $e=1$ and $k=2$ satisfies $N(a;1,2)=-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 table for the local dihedral length derivative. 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 of length $\sqrt{2}$, and one body diagonal of length $\sqrt{3}$.
The Schläfli identity expresses the differential of solid angle in terms of dihedral angles. After clearing the arccos radical via the Cayley-Menger cofactor discriminant, each summand becomes a pure rational function schlaefliPolySummandNorm of the six squared edges. Numerators and denominators are built from the explicit cofactor polynomials cmCofactor3Poly and their partials cmCofactorPartial, indexed by the pair of Cayley-Menger vertices opposite a chosen edge (oppositeCMVertices).
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 those polynomials together with freudenthalTetSqEdges and oppositeCMVertices (edge 1 opposite CM vertices $(2,4)$). Simplify the resulting expressions with the match-tables for cmCofactor3Poly and cmCofactorPartial, then close by norm_num, which evaluates the concrete rationals to $-2$.
why it matters
This is one cell of the lookup table that freudenthalSchlaefliPolySummandNorm_eq_table assembles by case analysis on $(e,k)$. That table is the algebraic backbone of the Freudenthal length-chain endpoint certificates: once every rationalized summand is a known constant, the closed-form dihedral length derivative dihedralClosedDerivLength becomes an explicit numeric matrix, and the local pair coefficient freudenthalLocalPairClosedFormSchlaefliCoeff is fully certified.
In the broader Recognition gravity stack these constants feed discrete curvature and length-response identities on the eight-tick cubic lattice (T7), where $D=3$ spatial dimensions (T8) are already forced. The certificate is pure geometry; it does not itself invoke the J-cost or the mass ladder, but it supplies the numeric input those layers later consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.