Geometry Cofactor Polynomial

Explicit polynomials for tetrahedra

The Cayley-Menger determinant is the classical tool for deciding whether six lengths can form a tetrahedron in ordinary three-dimensional space. It is a 5 by 5 determinant whose entries are 0, 1, and the six squared edge lengths. Its cofactors, the 4 by 4 subdeterminants, carry the same geometric information in a more flexible form: they appear naturally when one differentiates the volume formula or computes dihedral angles. A cofactor polynomial is simply one of these subdeterminants written out as an explicit polynomial in the six squared edge lengths, with no determinant left implicit.

The central result states that every one of the 25 cofactors of the Cayley-Menger matrix equals its explicitly expanded polynomial form. The expansion is complete: each cofactor becomes a sum of monomials in the six squared edge coordinates, with all coefficients written out. This matters because downstream calculations, especially dihedral-angle calculus, can then refer to named polynomial partials instead of opaque derivative terms. The same body of work also proves that the partial derivative of each cofactor polynomial along any one edge coordinate is given by a closed-form polynomial, so differentiation becomes a matter of reading off a coefficient rather than recomputing a limit.

In Recognition Science, this body of work is a workhorse for the recognition-to-linking bridge. The framework's forcing chain derives three spatial dimensions from a discrete recognition ledger, and tetrahedral geometry is the local shape of that space. Having explicit cofactor polynomials means the framework can compute how a tetrahedron's geometry responds to changes in its edge lengths, which is the kind of calculation needed to connect the discrete ledger to continuous spatial structure. The physical bridge itself remains open, but the algebraic machinery for the tetrahedral step is now explicit and machine-checked.

The practical payoff is that a computer can now evaluate any cofactor and its derivatives by direct polynomial arithmetic, with no determinant solver and no numerical differentiation. The theorems guarantee the polynomial forms agree with the determinant definitions for every choice of the six squared edge lengths. This turns a conceptually simple but algebraically heavy part of geometry into a routine, verifiable computation.

/-- 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

/-- Closed-form coordinate derivative of every cofactor polynomial. -/
theorem hasDerivAt_cmCofactor3Poly_along_coord
    (r c : Fin 5) (k : Fin 6) (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cmCofactor3Poly r c (Function.update a k t))
      (cmCofactorPartial r c k a) (a k) := by
  have hfun :
      (fun t : ℝ => cmCofactor3Poly r c (Function.update a k t)) =
        (fun t : ℝ => cmCofactor3Poly r c a
          + cmCofactorPartial r c k a * (t - a k)
          + cmCofactorQuadraticCoeff r c k a * (t - a k) ^ 2
          + 0 * (t - a k) ^ 3) := by
    funext t
    have h := cmCofactor3Poly_update_polyform r c a k (t - a k)
    have hbase : a k + (t - a k) = t := by ring
    rw [hbase] at h
    simpa using h
  rw [hfun]
  exact hasDerivAt_shifted_cubic (cmCofactor3Poly r c a)
    (cmCofactorPartial r c k a) (cmCofactorQuadraticCoeff r c k a) 0 (a k)

What this page does not claim

The body of work does not prove that the Cayley-Menger determinant vanishes for tetrahedra; it only expands the cofactors. The body of work does not establish the physical bridge from recognition events to continuous space.

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: