regular_cm_volume_identity
plain-language theorem explainer
The declaration equates the Cayley-Menger value of a regular tetrahedron with edge length a to 144 times the square of its classical volume V = a³√2/12. Recognition Science geometers cite it when linking edge-length data to volume forms inside simplicial complexes. The proof is a short tactic sequence that rewrites via the regular value equation then applies field simplification and ring normalization to confirm the algebraic match.
Claim. For a regular tetrahedron with edge length $a > 0$, let $V = (a^3 √2)/12$ be its Euclidean volume. The Cayley-Menger determinant value then satisfies cmData.value = 144 V².
background
The CayleyMenger module records the Cayley-Menger determinant as a scalar built directly from edge lengths for n-simplices, avoiding full matrix lifts. RegularTet is the structure with field a : ℝ and proof 0 < a; its cmData extracts the corresponding TetCMData whose value is the determinant expression. TetVolumeIdentity and TetCMData supply the surrounding data structures for tetrahedra.
proof idea
The proof rewrites the left side with regular_cm_value_eq. It introduces the fact Real.sqrt 2 ^ 2 = 2 via Real.sq_sqrt, simplifies the squared volume term to a^6 * 2 / 144 by field_simp and ring_nf, then finishes with a final ring normalization to reach equality.
why it matters
The result is packaged inside cayleyMengerCert, which supplies the regular volume identity to the dihedral-angle and Schläfli phases that discharge ReggeDeficitLinearizationHypothesis. It encodes the classical Cayley 1841 identity CM = 144 V² for the regular case, supporting the D = 3 spatial setting in the Recognition Science geometry bridge. The proof is complete with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.