local_dihedralDenom3Poly_ne_zero
plain-language theorem explainer
Nondegenerate tetrahedra in a finite 3D Regge triangulation yield a nonzero polynomial-cofactor denominator at every local dihedral angle. Continuity and smoothness arguments for the nonlinear Regge action cite this to keep arccos and cofactor expressions well-defined. The proof is a one-line wrapper: strict positivity already proved for the same denominator implies nonzeroness.
Claim. Let $K$ be a finite 3D Regge triangulation with nondegenerate squared-edge data on every tetrahedron. For each tetrahedron $\tau$ and each of the six edge indices $f$, the polynomial-cofactor dihedral denominator of $\tau$'s squared-edge tuple at $f$ is nonzero.
background
The module collects analytic inputs for the full nonlinear Regge action: the conformal edge chart must remain in the nondegenerate tetrahedral cone, arccos arguments must stay off $\pm 1$, and the finite action must be smooth at the flat potential. Those requirements are packaged as named configuration facts rather than axioms.
A Triangulation3D is a finite abstract 3D Regge complex whose every tetrahedron carries a nondegenerate squared-edge 6-tuple. The polynomial-cofactor denominator dihedralDenom3Poly is the square root of the product of the two diagonal Cayley-Menger polynomial cofactors at the pair of vertices opposite a chosen edge; it is definitionally lighter than the determinant-normalized denominator.
The immediate upstream fact is local positivity: on every tetrahedron of $K$ and every edge index, that polynomial denominator is strictly positive, by reduction to the nondegeneracy lemma for a single tetrahedron.
proof idea
One-line wrapper. Apply the standard real lemma that strict positivity implies nonzeroness (ne_of_gt) to the already-proved local positivity statement for the same triangulation, tetrahedron, and edge index. No further algebraic expansion of the cofactor polynomial is required.
why it matters
This lemma is the nonzero half of the local denominator package. Its sole direct consumer rewrites the normalized dihedral denominator as the polynomial form and invokes this fact, obtaining dihedralDenom3 \neq 0 on every local edge of every tetrahedron.
That nonvanishing is required before continuity of squared cosine of the dihedral angle can be stated at a configuration, and before the module's smoothness chain for the nonlinear Regge action at flat potentials can proceed. In the broader Recognition geometry stack it supports the analytic side of the closed second-order component story: the exact quadratic truncation is already controlled, and these denominator facts keep the full nonlinear action inside the smooth regime near flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.