regular_not_flat
plain-language theorem explainer
A regular tetrahedron with positive edge length a has strictly positive Cayley-Menger determinant and therefore cannot be flat. Workers on the simplicial phase of Recognition Science cite this to guarantee non-degeneracy when feeding regular configurations into dihedral-angle and deficit calculations. The argument substitutes the closed-form determinant value and invokes its positivity to reach an immediate contradiction with zero via linear arithmetic.
Claim. Let $R$ be a regular tetrahedron with edge length $a>0$. Then the Cayley-Menger value attached to $R$ is nonzero, so $R$ is not flat.
background
The module defines the Cayley-Menger determinant for a tetrahedron from its six edge lengths as a scalar built directly from those lengths. A RegularTet is the structure consisting of a single positive real $a$ that sets all six edges equal via the map toTetEdges. IsFlat is the predicate that holds exactly when the attached CM value equals zero. Upstream, regular_cm_value_eq supplies the explicit formula $2a^6$ while regular_cm_positive establishes that this quantity is positive for any such $R$.
proof idea
The proof unfolds IsFlat to expose the equality cm.value = 0. It rewrites using regular_cm_value_eq to replace the value with $2a^6$. The positivity theorem regular_cm_positive is applied to the same rewritten expression, yielding $0<2a^6$. Linear arithmetic then immediately rules out equality to zero.
why it matters
This result is collected inside the CayleyMengerCert structure together with the value formula, positivity, and volume identity. Downstream modules consume the certificate when constructing dihedral angles and applying Schläfli's identity. It directly supports the non-degeneracy assumption required for the simplicial deficit discharge in the Recognition Science chain from T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.