Geometry Cofactor Polynomial Cm Cofactor3 Opposite Diag Eq Poly

Cofactor polynomials

The Cayley-Menger matrix is the standard algebraic object that decides whether six lengths can form a tetrahedron and, if they can, what its volume is. Its entries are built from the six squared edge lengths and a row and column of ones. The cofactors of this matrix, obtained by deleting one row and one column and taking a determinant, appear in formulas for dihedral angles and other metric quantities of the tetrahedron.

The theorem cmCofactor3_opposite_diag_eq_poly states that a particular cofactor, the one associated with an entry on the opposite diagonal, equals an explicit polynomial in the six squared edge lengths. The polynomial is written out in full in the framework's machine-checked library of formal theorems. The statement holds for every assignment of six nonnegative real numbers to the edges, with no hidden geometric condition such as the triangle inequalities.

This is a computational convenience, not a new geometric fact. The cofactor was already a well-defined determinant; the theorem merely provides its expanded polynomial normal form. Downstream work on dihedral-angle calculus can then refer to named polynomial partials instead of opaque derivative terms. The framework's library also proves the matching statement for every other cofactor position, so the whole 5 by 5 array of cofactors is available in polynomial form.

What the theorem does not claim is that the polynomial has a geometric meaning on its own, nor that it vanishes for some special edge lengths. It also does not assert that the cofactor is nonzero, or that the tetrahedron exists. The equality is purely algebraic: it rewrites one determinant as a sum of products of the six variables. The existence and volume questions belong to the full Cayley-Menger determinant, not to this cofactor identity.

/-- Polynomial agreement for every diagonal cofactor used by tetrahedral
dihedral cosine denominators. -/
theorem cmCofactor3_opposite_diag_eq_poly
    (a : SqEdges) (e : Fin 6) (side : Bool) :
    let p := DihedralCayleyMenger.oppositeCMVertices e
    let r := if side then p.1 else p.2
    cmCofactor3 a r r = cmCofactor3Poly r r a := by
  fin_cases e <;> cases side
  · exact cmCofactor3_44_eq_poly a
  · exact cmCofactor3_33_eq_poly a
  · exact cmCofactor3_44_eq_poly a
  · exact cmCofactor3_22_eq_poly a
  · exact cmCofactor3_33_eq_poly a
  · exact cmCofactor3_22_eq_poly a
  · exact cmCofactor3_44_eq_poly a
  · exact cmCofactor3_11_eq_poly a
  · exact cmCofactor3_33_eq_poly a
  · exact cmCofactor3_11_eq_poly a
  · exact cmCofactor3_22_eq_poly a
  · exact cmCofactor3_11_eq_poly a

/-- Polynomial agreement for every diagonal cofactor used by tetrahedral
dihedral cosine denominators. -/
theorem cmCofactor3_opposite_diag_eq_poly
    (a : SqEdges) (e : Fin 6) (side : Bool) :
    let p := DihedralCayleyMenger.oppositeCMVertices e
    let r := if side then p.1 else p.2
    cmCofactor3 a r r = cmCofactor3Poly r r a := by
  fin_cases e <;> cases side
  · exact cmCofactor3_44_eq_poly a
  · exact cmCofactor3_33_eq_poly a
  · exact cmCofactor3_44_eq_poly a
  · exact cmCofactor3_22_eq_poly a
  · exact cmCofactor3_33_eq_poly a
  · exact cmCofactor3_22_eq_poly a
  · exact cmCofactor3_44_eq_poly a
  · exact cmCofactor3_11_eq_poly a
  · exact cmCofactor3_33_eq_poly a
  · exact cmCofactor3_11_eq_poly a
  · exact cmCofactor3_22_eq_poly a
  · exact cmCofactor3_11_eq_poly a

/-- The explicit polynomial normal form agrees with every determinant
cofactor of the tetrahedral Cayley-Menger matrix. -/
theorem cmCofactor3_eq_poly (a : SqEdges) (r c : Fin 5) :
    cmCofactor3 a r c = cmCofactor3Poly r c a := by
  fin_cases r <;> fin_cases c
  · exact cmCofactor3_00_eq_poly a
  · exact cmCofactor3_01_eq_poly a
  · exact cmCofactor3_02_eq_poly a
  · exact cmCofactor3_03_eq_poly a
  · exact cmCofactor3_04_eq_poly a
  · exact cmCofactor3_10_eq_poly a
  · exact cmCofactor3_11_eq_poly a
  · exact cmCofactor3_12_eq_poly a
  · exact cmCofactor3_13_eq_poly a
  · exact cmCofactor3_14_eq_poly a
  · exact cmCofactor3_20_eq_poly a
  · exact cmCofactor3_21_eq_poly a
  · exact cmCofactor3_22_eq_poly a
  · exact cmCofactor3_23_eq_poly a
  · exact cmCofactor3_24_eq_poly a
  · exact cmCofactor3_30_eq_poly a
  · exact cmCofactor3_31_eq_poly a
  · exact cmCofactor3_32_eq_poly a
  · exact cmCofactor3_33_eq_poly a
  · exact cmCofactor3_34_eq_poly a
  · exact cmCofactor3_40_eq_poly a
  · exact cmCofactor3_41_eq_poly a
  · exact cmCofactor3_42_eq_poly a
  · exact cmCofactor3_43_eq_poly a
  · exact cmCofactor3_44_eq_poly a

What this page does not claim

The polynomial has a geometric meaning on its own. The cofactor is nonzero for any particular edge lengths. The tetrahedron exists for the given edge lengths.

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