Pith. sign in
module module high

IndisputableMonolith.Geometry.CayleyMengerPolynomial

show as:
view Lean formalization →

Defines the tetrahedral Cayley-Menger polynomial cm3 as an explicit cubic in six squared edge lengths, plus the SqEdges type and basic analytic facts (continuity, ContDiff, scaling). Discrete-gravity and Regge authors cite it as the algebraic volume proxy before determinants or dihedral angles. The module is mostly definitions and direct polynomial identities, with short calculus lemmas for smoothness.

claimLet $a = (a_0,\ldots,a_5) \in \mathbb{R}^6$ be squared edge lengths of a tetrahedron. The module introduces $\mathrm{CM}_3(a)$, the explicit degree-3 Cayley-Menger polynomial in those six coordinates, together with the type of squared-edge 6-tuples, unit regular and right-angle reference configurations, and the statements that $\mathrm{CM}_3$ is $C^\infty$, continuous, and homogeneous of the expected degree under uniform edge scaling.

background

In classical geometry the squared volume of a tetrahedron is recovered from a $5\times 5$ Cayley-Menger determinant in the six edge lengths. Recognition Science discrete gravity works first with an explicit polynomial $\mathrm{CM}_3$ in the six squared lengths, so that gradients, Taylor expansions, and Regge variations can be written without expanding a determinant at every step.

This module fixes the coordinate convention: squared edges are indexed by $\mathrm{Fin},6$ (type SqEdges). It records two reference configurations (regular unit tetrahedron and right-angle unit tetrahedron) and evaluates $\mathrm{CM}_3$ on them. Calculus imports supply ContDiff and derivative infrastructure used to prove that evaluation of $\mathrm{CM}_3$ is smooth and continuous on $\mathbb{R}^6$, and that $\mathrm{CM}_3$ scales correctly when all squared lengths are multiplied by a common factor.

The local setting is pure Euclidean tetrahedron algebra: no Lorentzian signature and no mesh gluing yet. Downstream layers attach the actual determinant, partial derivatives, and realization in $\mathbb{R}^3$.

proof idea

Definition-heavy module. SqEdges and cm3 are introduced as data and an explicit cubic polynomial. Reference edge tuples (regular unit, right-angle unit) are concrete constants; their cm3 values are closed-form evaluations. Smoothness and continuity of cm3 follow from the ContDiff API for polynomials and arithmetic operations (contDiff_eval, then cm3_contDiff / cm3_continuous). Scaling and constant-square identities are direct algebraic rewrites of the cubic. No deep existence proof: the argument is "write the polynomial, check calculus and homogeneity lemmas."

why it matters in Recognition Science

This is the algebraic seed for the Regge component stack. ReggeRigorousFoundation bundles it as the explicit degree-3 polynomial needed to prove $M_{ij} = -\mathrm{area}(f_{ij})$ in 3D Regge calculus. CayleyMengerDerivatives builds the six partials and the polynomial Taylor identity for $\mathrm{cm3}(a+h)$ on top of it. CayleyMengerMatrix links cm3 to the $5\times 5$ determinant and cofactors for dihedral cosines. FourTetSignedDeficit uses the same squared-edge language for signed hinge deficits on abstract four-tet stars. TetrahedronRealization embeds the six coordinates into Euclidean 3-space. CausalSimplexWick imports the layer when moving from Euclidean tets to CDT-style causal classes in the Lorentzian Seven-Gaps lane. Without a single explicit cm3, those gradient, cofactor, and deficit theorems would each re-expand the determinant.

scope and limits

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (11)