Geometry Cayley Menger Matrix Regular Unit Vertex Diag Cofactor

The diagonal cofactor

The Cayley-Menger matrix is a square array built from the squared distances between points. For four points in ordinary space, it is a 5 by 5 matrix whose entries are 0 on the diagonal, 1 in the first row and column, and the six squared edge lengths in the remaining positions. Its determinant vanishes exactly when the four points can be embedded in three-dimensional space, which makes it a standard tool in distance geometry.

For a regular tetrahedron with all edges of length 1, the matrix takes a particularly simple form: every off-diagonal entry in the lower 4 by 4 block is 1. The cofactor of an entry is the signed determinant of the matrix left after deleting that entry's row and column. The declaration regularUnit_vertex_diag_cofactor proves that for any of the four non-zero rows, the diagonal cofactor equals -3. That is, if you delete the row and column of any of the four vertices, the determinant of the remaining 4 by 4 matrix, with the appropriate sign, is -3.

The theorem also shows the diagonal cofactor is the same for every vertex, a symmetry that reflects the tetrahedron's full rotational symmetry. The proof proceeds by reducing the minor to a fixed 4 by 4 matrix and computing its determinant directly. This result matters because the cofactors of the Cayley-Menger matrix feed into formulas for dihedral angles: the angle between two faces of the tetrahedron. Knowing the diagonal cofactor is a constant -3 gives a clean, checkable anchor for those formulas.

In Recognition Science, this declaration is a small but concrete piece of the framework's geometry library. It is a proved theorem, not a definition or a hypothesis. The framework's machine-checked library of formal theorems records that the computation is correct, with no gaps in the reasoning. The theorem does not, however, say anything about the off-diagonal cofactors, which are also computed in the library and take values of 1 or -1 depending on the position. It also does not connect the Cayley-Menger determinant to the framework's broader claims about recognition costs or the forcing of three dimensions; that bridge is a separate, open question.

/-- 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 det_regularUnitDiagMinorMatrix :
    Matrix.det regularUnitDiagMinorMatrix = -3 := by
  unfold regularUnitDiagMinorMatrix
  rw [Matrix.det_succ_row_zero]
  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]
  norm_num

What this page does not claim

The theorem does not determine the off-diagonal cofactors, which take values of 1 or -1 in the regular unit case. The theorem does not connect the Cayley-Menger determinant to the framework's forcing of three spatial dimensions. The theorem does not address the physical interpretation of the Cayley-Menger matrix in Recognition Science.

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: