Geometry Dihedral Cayley Menger Opposite Cmvertices

The opposite-vertex lookup

A tetrahedron has four triangular faces and six edges. Each edge sits between two vertices, and the remaining two vertices lie opposite that edge. The declaration oppositeCMVertices is a lookup table that records this pairing: for each of the six edges, it returns the two opposite vertices. It is a definition, not a theorem, a piece of bookkeeping that later formulas read from.

The table matters because of the Cayley-Menger matrix, a 5 by 5 array built from the six squared edge lengths of a tetrahedron. In that matrix the four vertices occupy rows and columns 1 through 4, not 0 through 3, so the lookup shifts each vertex index by one. The companion definition cmVertexIndex performs that shift, and oppositeCMVertices applies it to the opposite-vertex pairs. For the edge between vertices 0 and 1, for example, the table returns indices 3 and 4, which correspond to vertices 2 and 3.

The payoff appears in the dihedral cosine formula. For an edge e, let p and q be the opposite vertices. The classical cofactor formula reads cos θ_e = C_{p,q} / sqrt(C_{p,p} * C_{q,q}), where C is the cofactor matrix of the Cayley-Menger matrix. The definitions dihedralDenom3 and dihedralCos3Sq implement this formula directly, using oppositeCMVertices to supply p and q. This is the framework's machine-checked path from squared edge lengths to the angle between two faces of a tetrahedron.

What the declaration does not claim is just as important. It asserts nothing about geometry: no theorem says these are the correct opposite vertices, no proof shows the cofactor formula matches the usual dihedral angle. Those claims live in separate theorems, such as dihedralCos3_regularUnit, which proves that for a regular tetrahedron the cofactor formula gives cos θ = 1/3. The lookup table itself only names pairs; it is the surrounding theorems that give those pairs geometric meaning.

/-- For each tetrahedral edge, return the two Cayley-Menger vertex indices
opposite that edge. -/
def oppositeCMVertices : Fin 6 → Fin 5 × Fin 5
  | 0 => (3, 4) -- edge (0,1), opposite vertices 2,3
  | 1 => (2, 4) -- edge (0,2), opposite vertices 1,3
  | 2 => (2, 3) -- edge (0,3), opposite vertices 1,2
  | 3 => (1, 4) -- edge (1,2), opposite vertices 0,3
  | 4 => (1, 3) -- edge (1,3), opposite vertices 0,2
  | 5 => (1, 2) -- edge (2,3), opposite vertices 0,1

/-- Convert a tetrahedron vertex index `0..3` to the corresponding
Cayley-Menger matrix index `1..4`. -/
def cmVertexIndex : Fin 4 → Fin 5
  | 0 => 1
  | 1 => 2
  | 2 => 3
  | 3 => 4

/-- The tetrahedral dihedral cosine from Cayley-Menger cofactors. -/
def dihedralCos3Sq (a : SqEdges) (e : Fin 6) : ℝ :=
  let p := (oppositeCMVertices e).1
  let q := (oppositeCMVertices e).2
  cmCofactor3 a p q / dihedralDenom3 a e

/-- 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 assert that the opposite-vertex pairing is geometrically correct. The lookup table alone does not prove any formula for dihedral angles. No claim is made about the physical interpretation of the Cayley-Menger matrix.

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: