Geometry Cayley Menger Matrix Det Regular Unit Off Diag Minor Matrix13

A specific minor determinant

The Cayley-Menger matrix is a square table built from the squared distances between points. For a tetrahedron with six edges, the matrix has five rows and five columns: the first row and column are all ones, and the remaining entries are the squared edge lengths. Its determinant, the Cayley-Menger determinant, vanishes exactly when the six lengths can form a tetrahedron in ordinary three-dimensional space. This matrix is the standard tool for deciding whether a set of distances describes a real geometric object.

The declaration det_regularUnitOffDiagMinorMatrix13 concerns a specific 4 by 4 matrix obtained by deleting one row and one column from the 5 by 5 Cayley-Menger matrix of a regular tetrahedron with all edges of length 1. The theorem establishes that this particular minor has determinant 1. The matrix itself is written out explicitly: its entries are 0 on the diagonal and 1 elsewhere, except for one off-diagonal entry that is also 1, making it a near-complete all-ones matrix.

This determinant value is not an isolated curiosity. It feeds directly into the computation of cofactors, the signed minors used to invert matrices or expand determinants. In the framework's library, the theorem regularUnit_cofactor_13 uses this determinant to show that a particular cofactor of the regular tetrahedron's Cayley-Menger matrix equals 1. That cofactor, in turn, appears in the formula for the dihedral cosine of a regular tetrahedron, the angle between two faces. The chain of results connects a bare numeric determinant to a meaningful geometric quantity.

What the declaration does not claim is equally precise. It does not assert that the full 5 by 5 Cayley-Menger determinant of the regular tetrahedron equals 1; that determinant is 4, established separately. It does not generalize to arbitrary edge lengths or to other minors; each minor has its own value, some 1 and some -1. And it makes no statement about whether the matrix is invertible or about any physical significance of the number 1 beyond its role in the cofactor computation.

theorem det_regularUnitOffDiagMinorMatrix13 :
    Matrix.det regularUnitOffDiagMinorMatrix13 = 1 := by
  unfold regularUnitOffDiagMinorMatrix13
  rw [Matrix.det_succ_row_zero]
  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]

theorem regularUnit_cofactor_13 :
    cmCofactor3 regularUnitSqEdges 1 3 = 1 := by
  unfold cmCofactor3 cmCofactorSign3 cmMinor3
  simp [show Even (4 : Nat) by decide]
  rw [regularUnit_minor_13_eq_offDiag, det_regularUnitOffDiagMinorMatrix13]

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

What this page does not claim

The determinant of the full 5 by 5 Cayley-Menger matrix for the regular tetrahedron, which is 4, not 1. Any statement about the invertibility of the minor matrix or its physical significance beyond the cofactor computation. A generalization to arbitrary edge lengths or to other minors, each of which has its own determinant value.

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: