Geometry Dihedral Cayley Menger Dihedral Angle3 Regular Unit Of Cofactor Check

The regular tetrahedron check

A regular tetrahedron is the four-faced solid whose four vertices are all equally distant from one another. When each edge has length 1, the angle between any two faces is the same for all six edges, and its cosine is exactly 1/3. That value corresponds to an angle of about 70.53 degrees, a number familiar from solid geometry and chemistry, where it appears in molecules such as methane.

The classical route to this angle uses the Cayley-Menger matrix, a 5 by 5 array built from squared edge lengths that encodes the shape of a tetrahedron. Taking certain minors, called cofactors, of this matrix yields the cosine of the dihedral angle at each edge through the formula cos θ = C_p,q / sqrt(C_p,p C_q,q), where the indices p and q name the two vertices opposite the edge. This formula is standard in distance geometry, where it turns metric data into angle information.

The framework's machine-checked library of formal theorems contains a definition of this cofactor-based cosine and the corresponding angle. Its declaration dihedralAngle3_regularUnit_of_cofactorCheck proves that, for the regular unit tetrahedron, this cofactor angle equals the angle already defined by the existing regular-tetrahedron API. The proof runs through a check on the six cofactor values: for every edge, the off-diagonal cofactor is 1 and the two diagonal cofactors are both -3, which makes the cosine 1/3. A separate theorem, regularUnitCofactorCheck, establishes that these cofactor values hold without any external assumptions, so the equality is unconditional.

What this chain establishes is a consistency result: two independent ways of defining the dihedral angle of a regular unit tetrahedron agree. The cofactor formula, which works for any nondegenerate tetrahedron, reduces correctly to the known regular value. This matters because it validates the cofactor route as a trustworthy tool for angle computation in the framework's geometry library.

The declaration does not claim anything about tetrahedra that are not regular, nor does it assert that the cofactor formula is the only way to compute dihedral angles. It also makes no statement about the physical significance of the tetrahedron in any broader theory. The result is purely a piece of computational geometry: a proof that two definitions coincide on one special shape.

/-- Hence, under the regular cofactor check, the cofactor angle agrees with
the existing regular-tetrahedron dihedral API. -/
theorem dihedralAngle3_regularUnit_of_cofactorCheck
    (hC : RegularUnitCofactorCheck) (e : Fin 6) :
    dihedralAngle3 regularUnitTet e = regular_tet_dihedral.theta := by
  unfold dihedralAngle3 DihedralAngleData.theta regular_tet_dihedral
  rw [dihedralCos3_regularUnit_of_cofactorCheck hC e]

/-- The regular-unit cofactor check is now a theorem, not an assumption. -/
theorem regularUnitCofactorCheck : RegularUnitCofactorCheck := by
  intro e
  fin_cases e <;>
    simp [oppositeCMVertices,
      regularUnit_cofactor_34, regularUnit_cofactor_24, regularUnit_cofactor_23,
      regularUnit_cofactor_14, regularUnit_cofactor_13, regularUnit_cofactor_12,
      regularUnit_vertex_diag_cofactor]

/-- The cofactor formula gives the standard regular tetrahedron value
`cos θ = 1 / 3` without external assumptions. -/
theorem dihedralCos3_regularUnit (e : Fin 6) :
    dihedralCos3 regularUnitTet e = (1 / 3 : ℝ) :=
  dihedralCos3_regularUnit_of_cofactorCheck regularUnitCofactorCheck e

What this page does not claim

The declaration says nothing about tetrahedra with unequal edge lengths. It does not claim the cofactor formula is the only method for computing dihedral angles. It makes no statement about any physical or chemical meaning of the tetrahedron.

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/DihedralCayleyMenger.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: