cm3_conformalTetSqEdges_line_pos_eventually
plain-language theorem explainer
Along any real line of vertex potentials through the flat configuration, the Cayley–Menger cubic of each tetrahedron’s conformally rescaled squared edges stays strictly positive for all sufficiently small step sizes. Discrete-gravity and Regge-calculus workers cite this to keep tetrahedra non-degenerate under conformal deformations. The argument is pure continuity: the composite is continuous at zero and positive there, hence eventually positive in a neighborhood.
Claim. Let $K$ be a $3$-dimensional triangulation, $\xi$ a vertex potential on $K$, and $\tau$ any tetrahedron of $K$. Write $\eta_t$ for the linear path of potentials through the zero (flat) potential in the direction $\xi$. Then there exists a neighborhood of $t=0$ on which the Cayley–Menger polynomial $\mathrm{cm}_3$ evaluated on the six squared edge lengths of $\tau$ after conformal rescaling by $\eta_t$ is strictly positive.
background
The ambient module isolates the hard second-variation calculation for the nonlinear Regge action: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
The Cayley–Menger polynomial $\mathrm{cm}_3$ is the explicit degree-three polynomial in the six squared edge lengths of a tetrahedron; its sign controls oriented volume (positive volume iff $\mathrm{cm}_3>0$ for a non-degenerate tet). Each tetrahedron of the triangulation is assumed to satisfy $\mathrm{cm}_3>0$ at the flat (zero) potential. Conformal squared-edge maps send a vertex potential to the six squared lengths of a chosen tet after the standard conformal edge rescaling. The line potential is the straight-line path $t\mapsto t\xi$ through the zero potential.
Upstream smoothness facts supply that conformal squared edges are $C^\infty$ in the potential, and that $\mathrm{cm}_3$ itself is $C^\infty$ (hence continuous) on squared-edge space.
proof idea
Build continuity of the composite $t\mapsto\mathrm{cm}_3(\mathrm{conformalSqEdges}(K,\mathrm{linePotential}(K,\xi,t),\tau))$ at $t=0$, then push the strict inequality at zero into a neighborhood.
First, the line potential is $C^0$ (in fact $C^\infty$) at $0$ by componentwise fun_prop after rewriting with contDiffAt_pi. Second, conformal squared edges are ContDiffAt at the zero potential by the existing smoothness lemma for that map, rewritten via linePotential_zero. Compose those two facts to get ContDiffAt of the edge map along the line. Continuity of $\mathrm{cm}_3$ (from cm3_contDiff) then yields continuity of the full composite at $0$.
At $t=0$ the value equals $\mathrm{cm}_3$ of the undeformed tet, which is positive by the triangulation’s built-in cm_pos hypothesis (after simplifying with linePotential_zero and the zero-potential edge identity). Continuity plus membership of $(0,\infty)$ in the neighborhood filter of a positive number finishes the proof via ContinuousAt.eventually.
why it matters
Non-degeneracy of tetrahedra along conformal lines is a prerequisite for every local chain-rule identity that differentiates dihedral angles or Schläfli terms with respect to squared edges. Downstream, the result is fed directly into localConformalSchlaefliClosedFormZeroNearZero and into the flat-configuration form of the local conformal Schläfli angle–squared-edge chain rule near zero. Those targets assemble the second directional derivative of the nonlinear Regge action at the flat potential.
In the broader Recognition geometry stack this is scaffolding for the nonlinear Hessian theorem: once the second variation equals the canonical incidence Hessian, the Regge second-variation input package closes and the discrete Einstein–Hilbert picture sits on a fully rigorous second-order expansion. The argument itself is elementary analysis; its value is that it removes an open positivity obligation from every subsequent local conformal calculation near the flat sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.