Geometry Cayley Menger Matrix Det Regular Unit Off Diag Minor Matrix12

The off-diagonal minor

The Cayley-Menger matrix is a standard tool in geometry that encodes the squared distances between points. For a tetrahedron, this is a 5 by 5 matrix whose off-diagonal entries are the squared edge lengths, and whose first row and column are all ones except for the zero diagonal. The determinant of this matrix relates directly to the tetrahedron's volume, so understanding its structure is a way to study the shape of the tetrahedron through algebra.

This page concerns a specific 4 by 4 matrix called regularUnitOffDiagMinorMatrix12. It is a minor of the Cayley-Menger matrix for a regular tetrahedron with all edge lengths equal to one. The matrix is nearly the same as another minor, regularUnitDiagMinorMatrix, which has zeros on the diagonal and ones everywhere else. The matrix in question differs in exactly one entry: the entry in row two, column two is changed from zero to one.

The machine-checked library of formal theorems proves that the determinant of this specific matrix is negative one. This is a concrete, exact algebraic fact. It is not an approximation, and it does not depend on any numerical computation. The determinant is a signed quantity, and its negative sign is part of the result. This value is one of several similar determinants computed for minors of the same matrix, some of which equal one and others negative one.

In the framework of Recognition Science, this determinant is a building block. The library uses it to compute the cofactor of the original Cayley-Menger matrix at a particular position. The cofactor, in turn, is a component in the formula for the dihedral cosine of the tetrahedron. So this small determinant is not an isolated curiosity; it is a necessary step in a larger geometric calculation.

The declaration does not claim that this determinant is the volume of the tetrahedron, nor that it has any direct physical meaning on its own. It does not claim that the matrix represents any actual geometric configuration beyond the regular unit tetrahedron. The fact is purely algebraic: a specific 4 by 4 matrix, defined by a pattern of zeros and ones, has a determinant of negative one.

theorem det_regularUnitOffDiagMinorMatrix12 :
    Matrix.det regularUnitOffDiagMinorMatrix12 = -1 := by
  unfold regularUnitOffDiagMinorMatrix12
  rw [Matrix.det_succ_row_zero]
  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]

def regularUnitOffDiagMinorMatrix12 : Matrix (Fin 4) (Fin 4) ℝ :=
  !![(0 : ℝ), 1, 1, 1;
     1, 1, 1, 1;
     1, 1, 0, 1;
     1, 1, 1, 0]

What this page does not claim

The determinant of this matrix is not the volume of the tetrahedron. The matrix does not represent any geometric configuration other than the regular unit tetrahedron. The declaration does not establish a general formula for arbitrary Cayley-Menger minors.

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: