RegularTet
plain-language theorem explainer
RegularTet specifies a regular tetrahedron by a single positive real side length a. Downstream lemmas in the same module cite it to establish the Cayley-Menger scalar, its positivity, the volume identity, and non-flatness. The definition proceeds by direct construction: it builds a uniform TetEdges record with all lengths equal to a and packages the scalar 2 a^6 together with a trivial verification.
Claim. Let $a > 0$ be a positive real. A regular tetrahedron of side $a$ is the structure that equips the six edges of a tetrahedron with the constant length $a$ and records the associated Cayley-Menger scalar $2 a^6$.
background
The CayleyMenger module defines edge-length data and the Cayley-Menger scalar for tetrahedra as Phase C1 of the program to discharge ReggeDeficitLinearizationHypothesis. TetEdges is the structure that records six positive real lengths together with their positivity witness. The module adopts a minimal approach: it records the classical volume identity as a named hypothesis structure rather than reproving the full Euclidean geometry.
proof idea
The definition is a direct construction. toTetEdges sets every component of the Fin 6 length function to the common value a while copying the positivity hypothesis. cmData assigns the scalar 2 a^6 and discharges the regular_tet_value field by a single simp tactic that unfolds the uniform edge map.
why it matters
RegularTet supplies the concrete instance required by CayleyMengerCert, which packages the four Phase C1 results (value equality, positivity, volume identity, non-flatness). It therefore sits inside the simplicial geometry chain that feeds DihedralAngle, Schlaefli, and ultimately SimplicialDeficitDischarge. The construction touches the open question of extending the same identities from the regular case to arbitrary edge-length data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.