TetCMPositivity
plain-language theorem explainer
Defines the positivity of the Cayley-Menger determinant value for a tetrahedron given its six edge lengths. Workers on piecewise-flat geometry and simplicial Regge calculus cite it as the metric non-degeneracy criterion. The declaration is a one-line definition that directly asserts the supplied determinant is positive.
Claim. Let $T$ be edge-length data for a tetrahedron (six positive reals) and let $cm$ be the associated Cayley-Menger determinant data. The declaration states that $cm.value > 0$.
background
The module introduces the Cayley-Menger determinant for tetrahedra as Phase C1 toward discharging ReggeDeficitLinearizationHypothesis. TetEdges is the structure that records six positive real edge lengths together with their squares. TetCMData packages the determinant as a real scalar, recording its evaluation $2a^6$ when all edges equal $a$. The local setting treats positivity and the volume identity $288V^2=CM$ as named hypotheses rather than reproving the classical results of Cayley and Menger.
proof idea
The declaration is a one-line definition that directly states the inequality $0 < cm.value$.
why it matters
It supplies the non-degeneracy condition required by the volume identity hypothesis in the same module and is referenced by TetEdges constructions. The definition supports the chain through DihedralAngle and Schlaefli phases toward SimplicialDeficitDischarge. It aligns with the framework's pattern of importing classical geometry (D=3 simplices) as named hypotheses while keeping the RS bridge theorems zero-sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.