module module high

`IndisputableMonolith.Geometry.CayleyMengerMatrix`

Defines the 5×5 Cayley–Menger matrix of a tetrahedron as a smooth map of the six squared edge lengths, together with its determinant, principal minors, and cofactors. Geometers working on Regge calculus or tetrahedral realisability cite it as the concrete matrix layer under the Cayley–Menger polynomial. The module is mostly definitional, with short algebraic and continuity lemmas tying the matrix determinant back to the scalar CM polynomial.

claimFor squared edge lengths $s_{ij}\in\mathbb{R}$ of a tetrahedron, form the $5\times 5$ Cayley–Menger matrix $CM_3(s)$ with border row/column $(0,1,1,1,1)$ and interior block $-s_{ij}$. Write $\det CM_3$, the $4\times 4$ minors, and the signed cofactors as explicit functions of $s$, and record symmetry, continuity, and agreement with the scalar Cayley–Menger polynomial on standard configurations (regular and right-angled unit tetrahedra).

background

Classical Cayley–Menger geometry encodes the squared volume of a simplex in the determinant of a bordered matrix of squared distances. For a tetrahedron ($n=3$) one works with a $5\times 5$ matrix: a first row and column of the form $(0,1,1,1,1)$, and a $4\times 4$ interior block whose off-diagonal entries are the negatives of the six squared edge lengths.

The parent module CayleyMengerPolynomial opens the program of comparing the genuine Regge second-variation coefficient matrix $M_{ij}$, built from Cayley–Menger and dihedral-angle derivatives, componentwise to face areas. That comparison needs an explicit, differentiable matrix object rather than only a scalar polynomial.

This module supplies that object: named maps for the matrix, its determinant, minors, and cofactors, all as functions of the six squared-edge coordinates, with the usual Mathlib matrix and determinant infrastructure underneath.

proof idea

Primarily a definition module. The matrix is introduced entrywise from the six squared lengths; determinant, minors, and cofactors are the standard matrix constructions. Short lemmas prove symmetry of the matrix, identify the determinant with the scalar Cayley–Menger polynomial already defined upstream, evaluate the determinant on the regular and right-angled unit tetrahedra, and record $C^\infty$ dependence of entries, determinant, and minors on the edge coordinates via Mathlib continuity and differentiability facts for matrices.

why it matters in Recognition Science

This is the concrete matrix substrate for the tetrahedral Cayley–Menger calculus in the Recognition geometry stack. Downstream, CofactorPolynomial expands every cofactor into an explicit polynomial in the six squared edges so dihedral calculus can avoid opaque Fréchet derivatives. DihedralCayleyMenger defines tetrahedral dihedral cosines from those cofactors (replacing prose in the dihedral-angle development). GramCayleyMenger bridges the Euclidean Gram determinant of a realized tetrahedron to the Cayley–Menger determinant. RealisabilityCone carves the open domain of squared-edge tuples on which these formulas are meant to apply. Together they support the Regge second-variation comparison flagged in the upstream polynomial module: matching $M_{ij}$ against face areas component by component.

scope and limits

Does not prove the classical Cayley–Menger volume formula in full generality.
Does not define dihedral angles or their derivatives; those live downstream.
Does not construct the Regge Hessian $M_{ij}$ or compare it to face areas.
Does not characterize the full realisability region of six squared lengths.
Does not treat simplices other than the tetrahedron ($n=3$).

used by (4)

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

IndisputableMonolith.Geometry.CofactorPolynomial module_import
IndisputableMonolith.Geometry.DihedralCayleyMenger module_import
IndisputableMonolith.Geometry.GramCayleyMenger module_import
IndisputableMonolith.Geometry.RealisabilityCone module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMengerPolynomial module_import

declarations in this module (42)

def cmMatrix3 L42
def cmDet3 L66
def cmMinor3 L71
def cmCofactorSign3 L75
def cmCofactor3 L79
theorem cmMatrix3_symm L83
theorem cmDet3_eq_cm3 L90
theorem cmDet3_regular_unit L96
theorem cmDet3_rightAngle_unit L100
theorem cmDet3_contDiff L104
theorem cmMatrix3_entry_contDiff L113
theorem cmMinor3_contDiff L121
theorem cmCofactor3_contDiff L129
def regularUnitDiagMinorMatrix L141
def regularUnitOffDiagMinorMatrix L148
def regularUnitOffDiagMinorMatrix24 L154
def regularUnitOffDiagMinorMatrix23 L160
def regularUnitOffDiagMinorMatrix14 L166
def regularUnitOffDiagMinorMatrix13 L172
def regularUnitOffDiagMinorMatrix12 L178
theorem det_regularUnitDiagMinorMatrix L184
theorem det_regularUnitOffDiagMinorMatrix L191
theorem det_regularUnitOffDiagMinorMatrix24 L198
theorem det_regularUnitOffDiagMinorMatrix23 L204
theorem det_regularUnitOffDiagMinorMatrix14 L210
theorem det_regularUnitOffDiagMinorMatrix13 L216
theorem det_regularUnitOffDiagMinorMatrix12 L222
theorem regularUnit_minor_34_eq_offDiag L230
theorem regularUnit_cofactor_34 L238
theorem regularUnit_minor_24_eq_offDiag L245
theorem regularUnit_cofactor_24 L252
theorem regularUnit_minor_23_eq_offDiag L258
theorem regularUnit_cofactor_23 L265
theorem regularUnit_minor_14_eq_offDiag L272
theorem regularUnit_cofactor_14 L279
theorem regularUnit_minor_13_eq_offDiag L286
theorem regularUnit_cofactor_13 L293
theorem regularUnit_minor_12_eq_offDiag L299
theorem regularUnit_cofactor_12 L306
theorem regularUnit_diag_minor_eq_normalForm L315
theorem regularUnit_vertex_diag_cofactor L326
theorem cmDet3_scaling L335