snorm_zero_0_0
plain-language theorem explainer
The rationalized Schläfli summand on the Freudenthal unit-cube tetrahedron vanishes at edge-pair indices (0,0). Discrete-geometry and RS gravity workers cite it when filling the closed-form dihedral length-derivative table. The proof rewrites the summand as a cofactor ratio, unfolds the Freudenthal edge data, and evaluates to zero by simp and norm_num.
Claim. Let $a_{\mathrm{F}}$ be the squared-edge 6-tuple of a Freudenthal tetrahedron in the unit cube. The rationalized Schläfli summand at edge index $0$ and squared-edge coordinate $0$ is zero: $N_{\mathrm{Sch}}(a_{\mathrm{F}},0,0)=0$.
background
The module fully evaluates the rationalized Schläfli summand on the Freudenthal tetrahedron and records the induced closed-form table of dihedral length derivatives for the local-pair Schläfli coefficient.
A Freudenthal tetrahedron in the unit cube has squared edges three unit steps, two face diagonals, and one body diagonal (the fixed 6-tuple $a_{\mathrm{F}}$). Cayley-Menger cofactor polynomials give an algebraic normal form for every $3\times 3$ minor of the bordered squared-distance matrix; their partials with respect to each squared-edge coordinate are likewise explicit polynomials. For each tetrahedral edge, a fixed pair of opposite Cayley-Menger vertices selects the cofactors that enter the summand.
The rationalized Schläfli summand is the pure rational expression obtained after clearing the arccos radical by the cofactor discriminant. Up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, it equals the original polynomial-cofactor contribution. Its denominator is twice the product of the two opposite diagonal cofactors.
proof idea
Rewrite the summand via the numerator/denominator decomposition. Unfold the numerator, the denominator, the Freudenthal squared-edge tuple, and the opposite-vertex incidence map. The resulting expression is a concrete combination of cofactor polynomials and cofactor partials at the $(0,0)$ slot; simp matches those against their explicit polynomial clauses, and norm_num reduces the rational number to zero.
why it matters
This lemma is one cell of the $6\times 6$ certificate table. The parent result that the lookup table matches the evaluated rationalized summands dispatches on the edge-coordinate pair and quotes this fact for $(0,0)$. That table underwrites the closed-form dihedral length-derivative values used by the local-pair Schläfli coefficient in the Freudenthal length-chain endpoint certification.
In the Recognition framework the certificate sits on the geometric side of discrete 3-space: Freudenthal triangulation of the cube is the standard simplicial model compatible with $D=3$ (forcing step T8) and with eight-tick octave bookkeeping on the lattice. It does not itself touch the J-cost or mass ladder; it supplies the algebraic endpoint data those continuum limits later consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.