snorm_3_1
plain-language theorem explainer
The rationalized Schläfli summand on the Freudenthal tetrahedron, at edge index 3 and squared-edge coordinate 1, equals -2. Gravity and discrete-geometry workers cite this cell when assembling the 6×6 closed-form table that drives the local length-chain dihedral derivative. The proof rewrites the summand as a cofactor numerator over denominator, unfolds the Freudenthal edge data and opposite-vertex map, then finishes 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 of $a$ at edge index $e=3$ and squared-edge coordinate $k=1$ equals $-2$.
background
The module certifies every entry of the rationalized Schläfli summand on the local Freudenthal tetrahedron, then packages those values into the closed-form coefficient table used by the length-chain dihedral derivative.
A Freudenthal tetrahedron tiles the unit cube; its squared edges are the fixed tuple freudenthalTetSqEdges (unit steps, face diagonals, body diagonal). Dihedral geometry is read from Cayley-Menger cofactors: cmCofactor3Poly is the explicit polynomial normal form of each 3×3 cofactor, and cmCofactorPartial is its partial with respect to one squared-edge coordinate. For each tetrahedral edge, oppositeCMVertices names the two CM vertices opposite that edge.
The rationalized summand schlaefliPolySummandNorm removes the arccos radical via the cofactor discriminant. Up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, it is the pure rational expression whose numerator and denominator are built from those cofactors (schlaefliPolySummandNum / schlaefliPolySummandDen).
proof idea
Rewrite the summand via schlaefliPolySummandNorm_eq_num_div_den as numerator over denominator. Unfold the numerator and denominator definitions together with the Freudenthal squared-edge tuple and the opposite-vertex map for edge 3. Simplify the resulting cofactor polynomials and partials by the explicit match clauses of cmCofactor3Poly and cmCofactorPartial, then discharge the concrete rational arithmetic with norm_num to obtain $-2$.
why it matters
This is one cell of the full 6×6 evaluation demanded by the module. Downstream, freudenthalSchlaefliPolySummandNorm_eq_table matches on $(e,k)$ and cites each snorm_* lemma (including this one) to prove that the lookup table equals the evaluated rationalized summands. That table feeds the closed-form dihedralClosedDerivLength data for freudenthalLocalPairClosedFormSchlaefliCoeff, the local coefficient in the Freudenthal length-chain gravity analysis.
In the broader RS geometry stack the Freudenthal triangulation supplies the discrete 3-space scaffold consistent with the forced $D=3$ step of the forcing chain; certified Schläfli derivatives on that scaffold are the concrete input to continuum limits of recognition-length gravity. The declaration closes no open hypothesis: it is a finished numeric certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.