snorm_1_4
plain-language theorem explainer
Evaluates the rationalized Schläfli summand on the Freudenthal tetrahedron squared-edge data at edge index 1 and coordinate index 4, obtaining the constant 4. Gravity and discrete-geometry workers cite it when assembling the full 6×6 summand table. The proof rewrites the summand as a cofactor numerator over denominator, unfolds the Freudenthal edges 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 (three unit edges, two face diagonals, one body diagonal). The rationalized Schläfli summand of $a$ at edge index $e=1$ and squared-edge coordinate $k=4$ equals $4$.
background
The module certifies every entry of the $6\times 6$ matrix of rationalized Schläfli summands on the local Freudenthal tetrahedron, then feeds those values into a closed-form table for the length-derivative coefficients of the local pair Schläfli form.
A Freudenthal tetrahedron tiles the unit cube; its squared-edge data are fixed as $(1,2,3,1,2,3)$: three axis steps, two face diagonals, one space diagonal. The Schläfli identity expresses the differential of solid angle in terms of dihedral angles; after Cayley–Menger cofactors remove the arccos radical, each summand becomes a pure rational function schlaefliPolySummandNorm of the six squared edges.
That rational function is defined as a numerator (built from a $3\times 3$ cofactor and its partial in one edge coordinate) over a denominator $2,C_{pp}C_{qq}$, where $(p,q)$ are the two Cayley–Menger vertices opposite the chosen edge. Explicit polynomial normal forms for every cofactor and every partial are supplied by cmCofactor3Poly and cmCofactorPartial.
proof idea
One short computational certificate. Rewrite the summand via the identity that equates the normalized form to numerator over denominator. Unfold the numerator, the denominator, the Freudenthal squared-edge tuple, and the opposite-vertex pairing for edge 1. Simplify with the explicit cofactor and partial-cofactor polynomials, then close by norm_num, which evaluates the resulting rational expression to the integer 4.
why it matters
This is one cell of the full Freudenthal Schläfli-summand table. The parent theorem freudenthalSchlaefliPolySummandNorm_eq_table dispatches on $(e,k)$ and cites each snorm_* lemma; the present result covers the $(1,4)$ case. That table is the algebraic endpoint of the length-chain certificates used to obtain closed-form dihedral length derivatives for Freudenthal local pairs.
In the broader Recognition gravity stack these derivatives control how discrete edge lengths respond under the Schläfli constraint on the cube triangulation, so every nonzero table entry (including this constant 4) is load-bearing for the certified continuum limit of the length chain. No scaffolding remains: the claim is fully proved by exact arithmetic on the cofactor polynomials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.