snorm_4_1
plain-language theorem explainer
At the Freudenthal unit-cube tetrahedron, the rationalized Schläfli summand for edge 4 and squared-edge coordinate 1 equals 4. Gravity and discrete-geometry workers cite it when assembling the 6×6 closed-form coefficient table for local dihedral length derivatives. The proof rewrites the summand as numerator over denominator, unfolds the cofactor polynomials on the fixed edge lengths, 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 $e=4$ and squared-edge coordinate $k=1$ equals $4$.
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 local dihedral length derivatives used in the gravity length-chain.
A Freudenthal tetrahedron in the unit cube has fixed squared edges $a=(1,2,3,1,2,\ldots)$: three unit steps, two face diagonals, and one body diagonal. The Schläfli identity expresses dihedral-angle variation in terms of edge lengths; after clearing the arccos radical via the Cayley–Menger cofactor discriminant, each summand becomes a pure rational function schlaefliPolySummandNorm of the squared edges.
That rational form is numerator over denominator built from opposite-vertex cofactors: for each tetrahedral edge one takes the two Cayley–Menger indices opposite that edge, forms the $3\times 3$ cofactor polynomials and their partials in the squared-edge coordinates, and assembles the quotient. Upstream, cmCofactor3Poly and cmCofactorPartial supply the explicit polynomial normal forms.
proof idea
Term-mode proof by direct evaluation. 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 map for edge 4. Simplify with the concrete match clauses of cmCofactor3Poly and cmCofactorPartial, then close by norm_num, which reduces the resulting rational arithmetic to the integer 4.
why it matters
One cell of the certified $6\times 6$ table of rationalized Schläfli summands on the Freudenthal tetrahedron. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table dispatches on $(e,k)$ and cites this lemma for the $(4,1)$ case, so the lookup table is definitionally equal to the evaluated summands. That table feeds the closed-form coefficients of freudenthalLocalPairClosedFormSchlaefliCoeff and thence the discrete length-chain endpoint certificates in the gravity layer. In the Recognition geometry stack these local dihedral derivatives control how edge-length variations propagate through the eight-tick / cube triangulation scaffolding that underlies continuum limits; the certificate removes a numeric gap in that chain rather than introducing new physics axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.