TetCMData
plain-language theorem explainer
TetCMData packages the Cayley-Menger scalar for a tetrahedron's six edge lengths together with the conditional that the scalar equals 2a^6 on the regular case. Researchers on simplicial geometry and Regge calculus in Recognition Science cite it as the base carrier for volume and positivity hypotheses. The definition is a direct structure declaration with the regularity clause recorded as a field.
Claim. Let $T$ be edge-length data consisting of a map $e: {0,1,2,3,4,5} → ℝ^+$ with all values positive. A TetCMData instance for $T$ is a real number $v$ such that whenever all six lengths equal some $a > 0$, then $v = 2a^6$.
background
The module sets up the Cayley-Menger determinant for tetrahedra as Phase C1 of the program to discharge ReggeDeficitLinearizationHypothesis for simplicial complexes. TetEdges supplies the input data: a structure with field len : Fin 6 → ℝ together with the positivity axiom ∀e, 0 < len e. The CM value is introduced directly as a scalar polynomial in the squared lengths rather than via an explicit 5×5 matrix determinant.
proof idea
The declaration is a plain structure definition. It introduces two fields: the real scalar value and the conditional regular_tet_value that enforces the equality 2a^6 when all edges coincide. No lemmas or tactics are invoked.
why it matters
TetCMData is consumed directly by TetVolumeIdentity (which records 288 V² = CM) and TetCMPositivity (which records strict positivity on non-degenerate tetrahedra). It supplies the base data object for the geometry chain that later phases use for dihedral angles and Schläfli identities. The construction follows the module's pattern of treating the classical Cayley-Menger identity as a named hypothesis rather than reproving it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.