snorm_3_2
plain-language theorem explainer
The rationalized Schläfli summand on the Freudenthal tetrahedron, at edge index 3 and squared-edge coordinate 2, equals exactly 2. Discrete-geometry and RS gravity workers cite it as one cell of the 6×6 certificate table feeding the closed-form dihedral length derivative. Proof rewrites the summand as a cofactor ratio, unfolds the fixed Freudenthal edges, and finishes by numeric simplification.
Claim. For the fixed squared-edge 6-tuple of a Freudenthal tetrahedron in the unit cube, the rationalized Schläfli summand at edge $e=3$ and coordinate $k=2$ equals $2$.
background
The module certifies the full $6\times 6$ evaluation of the rationalized Schläfli summand on the Freudenthal tetrahedron, together with the induced closed-form dihedral length-derivative table.
A Freudenthal tetrahedron tiles the unit cube. Its squared-edge tuple is fixed: three unit-step edges, two face diagonals, and one body diagonal (values $1,2,3,1,2,3$). The Schläfli identity couples volume variation to dihedral angles; after the arccos radical is removed via the Cayley-Menger cofactor discriminant, each summand collapses to a pure rational function of the six squared edges.
That rational function is built from the explicit cofactor polynomials and their partial derivatives with respect to a chosen squared-edge coordinate, indexed by the pair of Cayley-Menger vertices opposite the selected tetrahedral edge.
proof idea
Rewrite the summand as numerator over denominator via the equality that identifies the rationalized form with that ratio. Unfold the numerator, the denominator, the Freudenthal squared-edge tuple, and the opposite-vertex map. Simplify against the match-clauses of the explicit cofactor polynomial and its partials, then close the resulting rational arithmetic by norm_num.
why it matters
This cell is one of the thirty-six concrete evaluations assembled by the table-matching theorem, which asserts that the lookup table equals every evaluated rationalized summand on the Freudenthal edges. That table supplies the closed-form coefficients for the local-pair Schläfli coefficient and the induced dihedral length-derivative table used in the gravity length-chain endpoint certificates.
In the Recognition Science gravity stack, Freudenthal triangulation of the cube is the discrete geometric substrate for local curvature and length-chain identities. These numeric certificates close the algebraic side of that substrate; without them the closed-form derivative table remains an unproved lookup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.