schlaefliCommonDenom_ne_zero
plain-language theorem explainer
On any nondegenerate tetrahedron the product of the six rationalized Schläfli summand denominators is nonzero. Anyone clearing those summands to a single polynomial identity cites this. The proof unfolds the product and applies the per-edge denominator nonvanishing lemma via the finite-product criterion.
Claim. If $T$ is a nondegenerate tetrahedron (positive squared edge lengths and positive Cayley–Menger volume), then the common Schläfli denominator $\prod_{e=1}^{6} d_e(T)$ is nonzero, where each $d_e$ is the rationalized denominator of the $e$-th Schläfli summand.
background
The module targets a closed-form local tetrahedral Schläfli identity: explicit Cayley–Menger volume derivatives and dihedral derivatives are packaged so the remaining work is one algebraic identity rather than an external analytic field.
A nondegenerate tetrahedron carries six positive squared edge lengths and a strictly positive Cayley–Menger 3-volume. The common denominator is the product, over the six edges, of the rationalized Schläfli summand denominators. Each individual factor is already known to be nonzero on nondegenerate tetrahedra (via the dihedral cofactor product polynomial nonvanishing lemma).
Clearing those six rational summands produces a single common numerator whose vanishing is the intended closed Schläfli equation. Nonvanishing of the product is the prerequisite that makes that clearing legitimate over $\mathbb{R}$.
proof idea
One-line structural argument. Unfold the common-denominator definition to a finite product over Fin 6. Apply Finset.prod_ne_zero_iff, reducing to pointwise nonvanishing. For each edge index, invoke the already-proved per-summand lemma that each rationalized Schläfli denominator is nonzero on a nondegenerate tetrahedron. No case splits or coordinate expansions appear at this layer.
why it matters
This is a bookkeeping gate in the closed-form tetrahedral Schläfli package. The module reduces the classical differential Schläfli relation on a tetrahedron to an explicit polynomial identity after clearing denominators; without a nonzero common denominator that reduction is undefined.
Downstream, the sibling common-numerator target (still open in the module comment) is meant to finish the identity by six coordinate-specific numerator lemmas rather than a global unfold. No parent theorem currently consumes this result in the graph, so it sits as infrastructure for that remaining closure.
In the broader Recognition geometry stack this supports rigorous Regge-style discrete curvature on nondegenerate tets, feeding dimensional and gluing arguments that ultimately sit under the forcing chain’s $D=3$ landmark, but the lemma itself is pure real-algebraic nondegeneracy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.