Geometry Cayley Menger Matrix

The Cayley-Menger matrix

The Cayley-Menger matrix is a square table built from the six squared edge lengths of a tetrahedron. For a tetrahedron with vertices 0, 1, 2, 3, the matrix has one extra row and column on top of the four vertices, so it is 5 by 5. The first row and column are all 1s except for a 0 in the corner; the remaining 4 by 4 block has 0s on its diagonal and the squared distances between vertices off the diagonal. This construction, named after Arthur Cayley and Karl Menger, is the standard way to decide from distances alone whether a set of points can be embedded in Euclidean space.

The matrix's determinant, called the Cayley-Menger determinant, carries the geometric information. For a tetrahedron the determinant is zero exactly when the six lengths are consistent with some tetrahedron in three-dimensional space. The determinant also scales predictably: multiplying every squared length by a factor s multiplies the determinant by s cubed. These facts were known classically; the framework's contribution is to formalize them in a machine-checked library of formal theorems, so that the determinant and its cofactors are available as a verified foundation for later geometric work.

In Recognition Science, the framework models physical structure as a discrete record of recognition events, and it uses this matrix as the determinant and cofactor layer for a dihedral cosine formula. The module proves that the 5 by 5 determinant equals a previously defined polynomial cm3, so the two descriptions agree. It also proves the determinant is infinitely differentiable as a function of the squared lengths, which matters for any calculus performed on it. For the regular tetrahedron with all edges of length 1, the determinant evaluates to 4; for a right-angle tetrahedron with mutually perpendicular edges of length 1, it evaluates to 8.

The cofactors of the matrix, which are signed determinants of 4 by 4 submatrices, are the algebraic pieces that appear in the dihedral cosine formula. The module proves explicit values for these cofactors on the regular unit tetrahedron: the diagonal cofactors are all -3, and the off-diagonal cofactors are all 1. These numbers are not arbitrary; they fall out of the matrix structure once the edge lengths are set to 1. The library shows the same cofactor values hold for every vertex, which is the symmetry one expects from a regular shape.

What this establishes in plain language is that the framework's geometric toolkit rests on a solid, verified base. The determinant and cofactor computations are not hand-waved; they are proved from the matrix definition by explicit calculation. This means that any later formula built on these cofactors, such as the dihedral cosine formula, inherits that rigor. The framework's library proves the classical determinant facts and the specific regular-tetrahedron values, so the geometry is not an assumption but a theorem.

/-- Mathlib's determinant of the Cayley-Menger matrix equals the explicit
polynomial `cm3`. -/
theorem cmDet3_eq_cm3 (a : SqEdges) : cmDet3 a = cm3 a := by
  unfold cmDet3 cmMatrix3 cm3
  simp [Matrix.det_succ_row_zero, Fin.sum_univ_succ, Fin.succAbove]
  ring_nf

/-- The determinant inherits the smoothness of the explicit polynomial. -/
theorem cmDet3_contDiff (n : ℕ∞) : ContDiff ℝ n cmDet3 := by
  have h : cmDet3 = cm3 := by
    funext a
    exact cmDet3_eq_cm3 a
  rw [h]
  exact cm3_contDiff n

/-- Regular unit tetrahedron determinant check. -/
theorem cmDet3_regular_unit : cmDet3 regularUnitSqEdges = 4 := by
  rw [cmDet3_eq_cm3, cm3_regular_unit]

/-- Right-angle unit tetrahedron determinant check. -/
theorem cmDet3_rightAngle_unit : cmDet3 rightAngleUnitSqEdges = 8 := by
  rw [cmDet3_eq_cm3, cm3_rightAngle_unit]

/-- The determinant inherits the cubic scaling law from `cm3`. -/
theorem cmDet3_scaling (a : SqEdges) (s : ℝ) :
    cmDet3 (fun e => s * a e) = s ^ 3 * cmDet3 a := by
  rw [cmDet3_eq_cm3, cm3_scaling, cmDet3_eq_cm3]

/-- Diagonal vertex cofactors of the regular unit tetrahedron. -/
theorem regularUnit_vertex_diag_cofactor (p : Fin 5) (hp : p ≠ 0) :
    cmCofactor3 regularUnitSqEdges p p = -3 := by
  unfold cmCofactor3 cmCofactorSign3 cmMinor3
  have heven : Even (p.val + p.val) := by
    use p.val
  simp [heven]
  rw [regularUnit_diag_minor_eq_normalForm p hp, det_regularUnitDiagMinorMatrix]

theorem regularUnit_cofactor_12 :
    cmCofactor3 regularUnitSqEdges 1 2 = 1 := by
  unfold cmCofactor3 cmCofactorSign3 cmMinor3
  simp [show ¬ Even (3 : Nat) by decide]
  rw [regularUnit_minor_12_eq_offDiag, det_regularUnitOffDiagMinorMatrix12]
  norm_num

What this page does not claim

This module does not prove that any six lengths form a tetrahedron; it only defines the matrix and its determinant. The framework's recognition-to-linking bridge for physical space is not established by this module.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/CayleyMengerMatrix.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: