schlaefliCommonDenom
plain-language theorem explainer
Defines the product of the six per-edge denominators that clear the rational Schläfli summands on a tetrahedron with squared edge lengths a. Anyone assembling the closed tetrahedral Schläfli identity after clearing fractions will cite it. The body is a plain finite product over Fin 6 of the individual summand denominators.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$, set $D(a):=\prod_{e=0}^{5} d_e(a)$, where $d_e(a)$ is the denominator of the rationalized Schläfli summand on edge $e$ (twice the product of the two opposite $3\times 3$ Cayley–Menger cofactor polynomials).
background
The module targets a closed-form tetrahedral Schläfli identity: explicit Cayley–Menger and dihedral derivative values feed a single algebraic equation rather than an external field. Squared edge lengths are packaged as SqEdges, i.e. maps $\mathrm{Fin},6\to\mathbb{R}$.
Each edge $e$ has a rationalized Schläfli summand whose denominator is $d_e(a)=2,C_{pp}(a),C_{qq}(a)$, with $p,q$ the opposite Cayley–Menger vertex pair for $e$ and $C_{\cdot\cdot}$ the degree-3 cofactor polynomials. The six summands must be put over a common denominator before the closed identity is stated as a polynomial equation.
Upstream, the per-edge denominator is exactly that cofactor product; the present definition multiplies them all.
proof idea
Pure definition: unfold to the product $\prod_{e:\mathrm{Fin},6} \texttt{schlaefliPolySummandDen},a,e$. No lemmas, no tactics.
why it matters
Clears fractions so the six rational Schläfli contributions become a single polynomial expression in the squared edges. The immediate consumer is the nonvanishing theorem: on a nondegenerate tetrahedron the common denominator is nonzero, so division is legitimate. That step sits inside the closed-form package (TetraSchlaefliClosedEquation and the squared-edge variant) that the module presents as the remaining hard identity linking Cayley–Menger volume data to dihedral derivatives. In the broader Recognition geometry layer this is bookkeeping infrastructure for the local Schläfli package, not a forcing-chain landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.