cayleyMengerCert
plain-language theorem explainer
Researchers working on the simplicial geometry bridge to Regge calculus cite cayleyMengerCert as the Phase C1 certificate that packages value, positivity, volume identity and non-flatness for regular tetrahedra. It supplies the classical input needed to discharge the linearization hypothesis without expanding the module by hundreds of lines. The proof is a term-mode structure instance that directly references four component lemmas.
Claim. Let $R$ be a regular tetrahedron of side length $a > 0$. The Cayley-Menger value of $R$ equals $2a^6$, is strictly positive, satisfies the identity $2a^6 = 144 ((a^3 sqrt(2)/12)^2)$, and $R$ is non-flat.
background
The module defines the Cayley-Menger determinant as a scalar built from edge lengths for $n$-simplices, with focus on tetrahedra, as Phase C1 toward discharging ReggeDeficitLinearizationHypothesis. It records the volume-from-CM identity as a named hypothesis structure rather than reproving classical piecewise-flat geometry. CayleyMengerCert is the structure that packages the four properties for regular tetrahedra: explicit value, positivity, volume identity, and non-flatness.
proof idea
The proof is a one-line wrapper that constructs the CayleyMengerCert instance by assigning regular_cm_value_eq to the value field, regular_cm_positive to the positivity field, regular_cm_volume_identity to the volume identity field, and regular_not_flat to the non-flat field.
why it matters
This declaration completes the packaging of Phase C1 results for the Cayley-Menger determinant. It feeds Phase C2 (DihedralAngle.lean) for cosine formulas and Phase C5 (SimplicialDeficitDischarge.lean) for the full chain to discharge ReggeDeficitLinearizationHypothesis. In the Recognition Science program it supplies the Euclidean geometry foundation for the piecewise-flat bridge without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.