IndisputableMonolith.Geometry.CayleyMengerPolynomial
Defines the tetrahedral Cayley–Menger polynomial cm3 as an explicit cubic in the six squared edge lengths, plus the Fin-6 squared-edge type and basic analytic facts (continuity, C^∞, scaling). Downstream geometry and Regge modules import it as the algebraic volume/defect engine. Content is definitional with direct evaluations on regular and right-angled unit tetrahedra.
claimIntroduce squared edge lengths $a \in \mathbb{R}^6$ for a tetrahedron and the Cayley–Menger polynomial $\mathrm{CM}_3(a)$, a degree-3 polynomial in those six coordinates. Record $\mathrm{CM}_3$ on the regular unit and right-angled unit edge sets, and prove that $\mathrm{CM}_3$ is $C^\infty$ (hence continuous) with the homogeneous scaling law under $a \mapsto \lambda^2 a$.
background
In classical distance geometry the squared volume of a tetrahedron is recovered from a $5\times 5$ Cayley–Menger determinant in the six edge lengths. This module works with the expanded polynomial form of that determinant: a single cubic $\mathrm{CM}_3$ in the six squared lengths, so that volume, rigidity, and later dihedral data can be treated by ordinary multivariable calculus rather than symbolic determinants at every step.
The ambient type is squared edges indexed by $\mathrm{Fin},6$ (three opposite pairs on $K_4$). Special points include the regular unit tetrahedron and a right-angled unit configuration, used as normalization checks. The module sits under the Geometry domain and is pure real analysis plus polynomial algebra; it does not yet attach Euclidean point realizations or Lorentzian edge signatures.
Downstream layers quote this polynomial as the algebraic core of 3D Regge calculus and of the certified Euclidean-to-causal tetrahedron bridge.
proof idea
Definition module. The squared-edge type and $\mathrm{CM}_3$ are introduced by explicit polynomial formulas. Closed-form evaluations on the regular and right-angled unit edge sets are direct substitution. Smoothness and continuity are obtained by composing the polynomial with the standard $C^\infty$ structure on $\mathbb{R}^6$ (via Mathlib contDiff/deriv infrastructure). Scaling identities follow from homogeneous degree counting in the cubic monomials.
why it matters in Recognition Science
This is the shared algebraic substrate for the tetrahedral geometry stack. CayleyMengerDerivatives imports it to expand $\mathrm{cm3}(a+h)$ into gradient, quadratic, and cubic remainder and to expose $\partial\mathrm{CM}3/\partial a_i$. CayleyMengerMatrix reconnects the polynomial to the $5\times 5$ determinant and cofactors needed for dihedral cosines. ReggeRigorousFoundation cites it as item (1) in the bundle proving the genuine Regge component theorem $M{ij}=-\mathrm{area}(f_{ij})$ in 3D. TetrahedronRealization lifts the six squared-edge coordinates to points in Euclidean 3-space. CausalSimplexWick reuses the same edge algebra when building certified Lorentzian (CDT-style) tetrahedron classes in $D=3$. In the broader Recognition chain this supports discrete gravity and the $D=3$ spatial forcing (T8) rather than the J-cost or $\varphi$-ladder layers directly.
scope and limits
- Does not prove that $\mathrm{CM}_3>0$ implies a nondegenerate Euclidean embedding.
- Does not define the $5\times 5$ Cayley–Menger matrix or its cofactors.
- Does not compute partial derivatives or the Taylor identity in $h$.
- Does not treat Lorentzian or CDT edge-type assignments.
- Does not state the Regge component theorem $M_{ij}=-\mathrm{area}(f_{ij})$.