Geometry Cayley Menger Matrix Det Regular Unit Off Diag Minor Matrix

A particular minor

The Cayley-Menger matrix is a square array built from the squared distances between points. For a tetrahedron, it is a 5 by 5 matrix whose off-diagonal entries are the six squared edge lengths, with a row and column of ones along the top and left. Its determinant, up to a constant factor, gives the squared volume of the tetrahedron. The declaration det_regularUnitOffDiagMinorMatrix concerns a specific 4 by 4 submatrix, called a minor, obtained by deleting one row and one column from the full 5 by 5 matrix.

That particular minor arises when the tetrahedron is regular, meaning all six edges have length 1, and when one deletes the row and column corresponding to a specific edge. The declaration states that the determinant of this 4 by 4 matrix equals -1. The matrix itself is displayed in the library: it has zeros on the diagonal and ones everywhere else, except for a single off-diagonal entry that is also 1, making it a nearly uniform array. The proof is a direct computation, expanding the determinant along the first row and simplifying the resulting 3 by 3 determinants.

The result is not an isolated curiosity. It feeds into a larger set of cofactor calculations for the regular tetrahedron. A cofactor is a signed minor, and the library proves that the cofactor for the same edge position equals 1, since the sign from the row and column indices is positive. This cofactor, in turn, is a component in the formula for the dihedral cosine, the angle between two faces of the tetrahedron. The determinant value of -1 is therefore a precise, verified input to a geometric formula, not a standalone fact.

In Recognition Science, this declaration is part of a machine-checked library of formal theorems, a collection where every statement is verified by a computer proof checker. The declaration is a definition of a matrix, and the theorem about its determinant is proved from that definition. It does not, however, make any claim about the physical world, about the nature of space, or about the framework's broader forcing chain. It is a piece of pure, classical geometry, formalized and checked, with no empirical content and no connection to the framework's cost function or constants.

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

/-- The off-diagonal vertex minor of the regular unit Cayley-Menger matrix. -/
def regularUnitOffDiagMinorMatrix : Matrix (Fin 4) (Fin 4) ℝ :=
  !![(0 : ℝ), 1, 1, 1;
     1, 0, 1, 1;
     1, 1, 0, 1;
     1, 1, 1, 1]

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

/-- First off-diagonal regular unit cofactor. -/
theorem regularUnit_cofactor_34 :
    cmCofactor3 regularUnitSqEdges 3 4 = 1 := by
  unfold cmCofactor3 cmCofactorSign3 cmMinor3
  simp [show ¬ Even (7 : Nat) by decide]
  rw [regularUnit_minor_34_eq_offDiag, det_regularUnitOffDiagMinorMatrix]
  norm_num

What this page does not claim

This declaration does not claim anything about the physical properties of a regular tetrahedron in space. It does not claim that the framework's forcing chain or its constants are derived from this determinant. It does not claim that the minor matrix represents any measurable quantity outside of the formal library.

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: