regular_cm_value_eq
plain-language theorem explainer
For a regular tetrahedron with edge length a the Cayley-Menger value equals exactly 2 a^6. Downstream lemmas in the same module cite this equality to obtain positivity and non-flatness. The proof is a single reflexivity reduction from the definition of cmData on RegularTet.
Claim. Let $R$ be a regular tetrahedron with edge length $a > 0$. Then the Cayley-Menger determinant value satisfies $R.cmData.value = 2 a^6$.
background
The module constructs the Cayley-Menger scalar directly from edge lengths for 3- and 4-simplices, recording volume identities as named hypothesis structures rather than full classical proofs. RegularTet is the structure with field a : ℝ and proof a_pos : 0 < a; its toTetEdges method assigns the same length to all six edges. The cmData field packages those lengths together with the resulting determinant scalar. The local setting is Phase C1 of the program to discharge ReggeDeficitLinearizationHypothesis for simplicial complexes.
proof idea
One-line reflexivity proof that matches the definition of cmData.value for any RegularTet instance.
why it matters
This equality supplies the regular_value field of cayleyMengerCert, which aggregates the four regular-case facts used by regular_cm_positive, regular_cm_volume_identity and regular_not_flat. It fills the explicit scalar step in Phase C1 before the dihedral-angle and Schläfli identities of Phases C2–C3. The factor of 2 is the normalization chosen so that the CM convention satisfies 144 V² = CM value for the classical volume V = a³ √2 / 12.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.