Geometry Cayley Menger Matrix Det Regular Unit Off Diag Minor Matrix23

A minor determinant in a tetrahedron matrix

The Cayley-Menger matrix is a standard tool in geometry: a symmetric table of squared distances that encodes whether a set of points can form a simplex, and what its volume is. For a tetrahedron, the matrix is 5 by 5, with zeros on the diagonal, ones in the first row and column, and the six squared edge lengths filling the rest. The determinant of this matrix, divided by 288, gives the square of the tetrahedron's volume, a result known since the 19th century.

When the tetrahedron is regular with all edges of length 1, the full 5 by 5 determinant equals 4, a fact the machine-checked library proves directly. The declaration det_regularUnitOffDiagMinorMatrix23 examines a smaller piece: delete row 2 and column 3 from the matrix, leaving a 4 by 4 table. That submatrix has ones almost everywhere except zeros in two positions. Its determinant is exactly -1.

This value is not an isolated curiosity. The same library computes the determinants of all six off-diagonal minors for the regular unit tetrahedron. Four of them, including this one, equal -1; the remaining two equal +1. These numbers feed directly into the cofactor formula for the inverse matrix, which in turn appears in the dihedral cosine formula, the angle between two faces of the tetrahedron. A cofactor is a signed minor, and the sign pattern here makes every off-diagonal cofactor equal to 1 for the regular unit tetrahedron.

The declaration itself is a definition, not a theorem about the physical world. It states what the determinant of that particular 4 by 4 matrix is, nothing more. It does not claim that the regular tetrahedron is the only shape with this property, nor does it connect the value -1 to any physical constant or recognition process. The result belongs to the classical geometry of the Cayley-Menger determinant, and the library's contribution is to verify the arithmetic by machine rather than by hand.

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

/-- 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 value -1 does not describe any physical property of a real tetrahedron. The declaration does not relate to the Recognition Science framework's cost function or forcing chain. No claim is made about the determinant of minors for tetrahedra with unequal edge lengths.

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: