regular_cm_positive
plain-language theorem explainer
Positivity of the Cayley-Menger determinant for a regular tetrahedron with edge length a > 0 holds unconditionally. Workers on the Recognition Science simplicial geometry pipeline cite this to guarantee non-degenerate volume contributions in Phase C1. The proof is a one-line term reduction that rewrites the value via regular_cm_value_eq and applies multiplication and power positivity.
Claim. For a regular tetrahedron with positive edge length $a$, the Cayley-Menger determinant satisfies $0 < 2a^6$.
background
The Cayley-Menger module defines TetEdges and TetCMData structures to encode simplex volumes from edge lengths as scalars, avoiding full matrix lifts. A RegularTet is the structure with field a : ℝ and a_pos : 0 < a, together with the map toTetEdges that sets all six lengths equal to a. The cmData.value is the scalar determinant built from these lengths. The module takes a minimal approach for Phase C1 of discharging ReggeDeficitLinearizationHypothesis: it records volume identities as named hypotheses rather than reproving classical Euclidean geometry.
proof idea
The term proof rewrites the goal with regular_cm_value_eq to obtain 0 < 2 * a^6, then applies exact mul_pos (norm_num for 2 > 0) (pow_pos R.a_pos 6).
why it matters
This supplies the regular_positive field inside cayleyMengerCert, which aggregates the regular tetrahedron properties for downstream use in regular_not_flat and the simplicial deficit chain. It fills the unconditional positivity step in the Cayley-Menger setup that supports dihedral angles and Schläfli identities in later phases. The result aligns with the framework's T8 forcing of D = 3 and the minimal-axiom pattern used for Regge linearization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.