Geometry Dihedral Cayley Menger Dihedral Cos3 Regular Unit Of Cofactor Check

The cofactor formula's payoff

In geometry, the dihedral angle of a tetrahedron is the angle between two faces meeting along an edge. For a regular tetrahedron, all six such angles are equal, and the cosine of that angle is exactly 1/3. The Cayley-Menger matrix is a 5 by 5 array built from squared edge lengths; its cofactors encode the tetrahedron's metric structure. A classical formula expresses the cosine of the dihedral angle at an edge as a ratio of cofactors, one off-diagonal divided by the square root of a product of diagonals.

This declaration, dihedralCos3_regularUnit_of_cofactorCheck, proves in the framework's machine-checked library of formal theorems that, for a regular tetrahedron with unit edges, this cofactor formula returns the value 1/3 for every one of the six edges. The proof proceeds by a finite case analysis over the six edges, using pre-established lemmas about the specific cofactor values for the unit regular tetrahedron. It is a theorem, not an assumption: the library previously treated the needed cofactor values as a check to be performed, and this declaration turns that check into a proved fact.

In Recognition Science, this is a small but load-bearing step. The framework derives physical constants from a forcing chain, and this result shows that a standard geometric formula, the Cayley-Menger cofactor expression, is consistent with the framework's own definition of a regular tetrahedron. It also connects the cofactor-based angle to the existing dihedral angle API, so downstream modules can rely on either formulation interchangeably.

What the declaration does not claim is broader. It does not prove the cofactor formula in general, nor does it derive the 1/3 value from first principles of the framework's forcing chain. It only establishes the value for the specific regular unit tetrahedron, under the explicit cofactor check. The general formula for arbitrary tetrahedra, and any claim about the physical significance of the dihedral angle, remain outside this declaration's scope.

/-- 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 does not prove the cofactor formula for arbitrary tetrahedra. It does not derive the 1/3 value from the framework's forcing chain. It makes no claim about the physical significance of the dihedral angle.

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: