Geometry Dihedral Cofactor Formula Cm Cofactor3 Edge0 Right Diag Eq Neg Four Nor

A tetrahedron's hidden square

In ordinary three-dimensional geometry, a tetrahedron is a pyramid with four triangular faces. Each face has an area, and each pair of faces meets along an edge, forming a dihedral angle. The classical question is how to compute that angle from the six edge lengths alone, without coordinates. The answer begins with a formula named after Marcel Berger, which expresses the cosine of a dihedral angle as a ratio of two cofactor expressions built from the squared edge lengths.

The declaration cmCofactor3_edge0_right_diag_eq_neg_four_normalSq is a small but necessary piece of that formula. It states that for edge 0 of a tetrahedron, a particular cofactor entry, the one in position (4,4) of a 6 by 6 matrix, equals negative four times the squared area of the opposite face. The cofactor here is a number computed from the six squared edge lengths by a fixed algebraic recipe. The theorem is proved in the machine-checked library of formal theorems, meaning a computer verified every step of the derivation.

The fact matters because it connects two different ways of describing a tetrahedron. One description uses the face normals, the perpendicular vectors to each face, whose dot products give the dihedral cosine. The other description uses only the squared edge lengths, arranged in a Gram matrix. The Berger cofactor formula says these two descriptions agree. The declaration supplies the specific identity that makes the agreement work for the right face of edge 0, by matching the squared normal length to a cofactor entry.

What the declaration does not claim is broader. It does not by itself prove the full Berger formula for all six edges; that is a separate theorem in the same module. It does not say anything about the physical meaning of tetrahedra in Recognition Science, nor does it involve the framework's cost function or recognition ledger. It is purely a statement of Euclidean geometry, verified by the framework's library, and it stands on its own as a geometric identity.

/-- Edge `0`: the second adjacent face-normal square in Gram entries. -/
theorem faceNormal_edge0_right_self_gram (T : RealizedTet) :
    faceNormal T 0 1 3 ⬝ᵥ faceNormal T 0 1 3 =
      gram3 T 0 0 * gram3 T 2 2 - gram3 T 0 2 * gram3 T 2 0 := by
  rw [faceNormal_dot_self]
  simp [coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]

set_option maxHeartbeats 2000000

/-- Edge `0`: the second adjacent face-normal square in Gram entries. -/
theorem faceNormal_edge0_right_self_gram (T : RealizedTet) :
    faceNormal T 0 1 3 ⬝ᵥ faceNormal T 0 1 3 =
      gram3 T 0 0 * gram3 T 2 2 - gram3 T 0 2 * gram3 T 2 0 := by
  rw [faceNormal_dot_self]
  simp [coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, edgeVector]

set_option maxHeartbeats 2000000

/-- The theorem target is discharged. -/
theorem bergerCofactorFormula3 : BergerCofactorFormula3 :=
  geometricDihedralCos_eq_cmCofactorRatio

What this page does not claim

This declaration does not establish the Berger formula for any edge other than edge 0. It does not involve the Recognition Science cost function or recognition ledger. It does not assign any physical meaning to tetrahedra beyond Euclidean geometry.

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