Encyclopedia Geometry Geometry Cofactor Polynomial Cm Cofactor3 Poly 34 Update Polyform

ARTICLE 3 claims 2 theorems 1 model

Geometry Cofactor Polynomial Cm Cofactor3 Poly 34 Update Polyform

A machine-checked library rewrites every tetrahedral cofactor into a plain polynomial, so angle calculus can stop wrestling with opaque derivative terms.

Verify this page

The explicit cofactor polynomial

A cofactor of a matrix is the signed determinant you get by deleting one row and one column. For a tetrahedron, the Cayley-Menger matrix encodes the six squared edge lengths, and its cofactors carry the geometry of the tetrahedron's angles and volume. The declaration cmCofactor3Poly_34_update_polyform is not a new theorem about geometry; it is a definition that names one specific polynomial: the cofactor in row 3, column 4 of the 5 by 5 Cayley-Menger matrix, written out as an explicit polynomial in the six squared edge coordinates.

Why does that matter? The framework's library of formal theorems works with recognition, a discrete record of events, but it also builds ordinary geometry. Downstream calculus on dihedral angles needs derivatives of these cofactors. Before this definition, those derivatives were opaque fderiv terms, hard to inspect or reason about. Now a derivative of the cofactor along one edge coordinate is itself a named polynomial, cmCofactorPartial, and the library proves that this derivative exists and equals that polynomial. The payoff is that angle calculus can refer to named polynomial partials instead of wrestling with abstract derivative objects.

The library also proves the cofactor polynomial agrees with the original cofactor: cmCofactor3_eq_poly states that for every tetrahedron and every row and column, the original cofactor equals the explicit polynomial. That is a theorem, machine-checked. The definition itself is a model: a choice of how to represent the cofactor. The agreement theorem is what turns that choice into a usable fact.

What the declaration does not claim is just as important. It does not prove any new geometric fact about tetrahedra, such as a formula for volume or an angle. It does not say anything about the golden ratio or the framework's forcing chain. It is a workhorse definition, not a discovery. Its value is organizational: it makes a piece of calculus explicit and checkable, so that later results can build on named, inspectable formulas instead of buried derivative terms.

MODEL cmCofactor3Poly · IndisputableMonolith/Geometry/CofactorPolynomial.lean
cmCofactor3Poly · IndisputableMonolith/Geometry/CofactorPolynomial.lean:26 
/-- Explicit polynomial normal form for every Cayley-Menger cofactor. -/
def cmCofactor3Poly (r c : Fin 5) (a : SqEdges) : ℝ :=
  match r.val, c.val with
  | 0, 0 => (a 2) ^ 2 * (a 3) ^ 2 - 2 * (a 1) * (a 2) * (a 3) * (a 4) + (a 1) ^ 2 * (a 4) ^ 2 - 2 * (a 0) * (a 2) * (a 3) * (a 5) - 2 * (a 0) * (a 1) * (a 4) * (a 5) + (a 0) ^ 2 * (a 5) ^ 2
  | 0, 1 => -2 * (a 3) * (a 4) * (a 5) + (a 2) * (a 3) * (a 5) + (a 2) * (a 3) * (a 4) - (a 2) * (a 3) ^ 2 + (a 1) * (a 4) * (a 5) - (a 1) * (a 4) ^ 2 + (a 1) * (a 3) * (a 4) - (a 0) * (a 5) ^ 2 + (a 0) * (a 4) * (a 5) + (a 0) * (a 3) * (a 5)
  | 0, 2 => (a 2) * (a 3) * (a 5) - (a 2) ^ 2 * (a 3) + (a 1) * (a 4) * (a 5) - 2 * (a 1) * (a 2) * (a 5) + (a 1) * (a 2) * (a 4) + (a 1) * (a 2) * (a 3) - (a 1) ^ 2 * (a 4) - (a 0) * (a 5) ^ 2 + (a 0) * (a 2) * (a 5) + (a 0) * (a 1) * (a 5)
  | 0, 3 => (a 2) * (a 3) * (a 4) - (a 2) ^ 2 * (a 3) - (a 1) * (a 4) ^ 2 + (a 1) * (a 2) * (a 4) + (a 0) * (a 4) * (a 5) + (a 0) * (a 2) * (a 5) - 2 * (a 0) * (a 2) * (a 4) + (a 0) * (a 2) * (a 3) + (a 0) * (a 1) * (a 4) - (a 0) ^ 2 * (a 5)
  | 0, 4 => -(a 2) * (a 3) ^ 2 + (a 1) * (a 3) * (a 4) + (a 1) * (a 2) * (a 3) - (a 1) ^ 2 * (a 4) + (a 0) * (a 3) * (a 5) + (a 0) * (a 2) * (a 3) + (a 0) * (a 1) * (a 5) + (a 0) * (a 1) * (a 4) - 2 * (a 0) * (a 1) * (a 3) - (a 0) ^ 2 * (a 5)
  | 1, 0 => -2 * (a 3) * (a 4) * (a 5) + (a 2) * (a 3) * (a 5) + (a 2) * (a 3) * (a 4) - (a 2) * (a 3) ^ 2 + (a 1) * (a 4) * (a 5) - (a 1) * (a 4) ^ 2 + (a 1) * (a 3) * (a 4) - (a 0) * (a 5) ^ 2 + (a 0) * (a 4) * (a 5) + (a 0) * (a 3) * (a 5)
  | 1, 1 => (a 5) ^ 2 - 2 * (a 4) * (a 5) + (a 4) ^ 2 - 2 * (a 3) * (a 5) - 2 * (a 3) * (a 4) + (a 3) ^ 2
  | 1, 2 => -(a 5) ^ 2 + (a 4) * (a 5) + (a 3) * (a 5) + (a 2) * (a 5) - (a 2) * (a 4) + (a 2) * (a 3) + (a 1) * (a 5) + (a 1) * (a 4) - (a 1) * (a 3) - 2 * (a 0) * (a 5)
  | 1, 3 => (a 4) * (a 5) - (a 4) ^ 2 + (a 3) * (a 4) - (a 2) * (a 5) + (a 2) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5) + (a 0) * (a 4) - (a 0) * (a 3)
  | 1, 4 => (a 3) * (a 5) + (a 3) * (a 4) - (a 3) ^ 2 - 2 * (a 2) * (a 3) - (a 1) * (a 5) + (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5) - (a 0) * (a 4) + (a 0) * (a 3)
  | 2, 0 => (a 2) * (a 3) * (a 5) - (a 2) ^ 2 * (a 3) + (a 1) * (a 4) * (a 5) - 2 * (a 1) * (a 2) * (a 5) + (a 1) * (a 2) * (a 4) + (a 1) * (a 2) * (a 3) - (a 1) ^ 2 * (a 4) - (a 0) * (a 5) ^ 2 + (a 0) * (a 2) * (a 5) + (a 0) * (a 1) * (a 5)
  | 2, 1 => -(a 5) ^ 2 + (a 4) * (a 5) + (a 3) * (a 5) + (a 2) * (a 5) - (a 2) * (a 4) + (a 2) * (a 3) + (a 1) * (a 5) + (a 1) * (a 4) - (a 1) * (a 3) - 2 * (a 0) * (a 5)
  | 2, 2 => (a 5) ^ 2 - 2 * (a 2) * (a 5) + (a 2) ^ 2 - 2 * (a 1) * (a 5) - 2 * (a 1) * (a 2) + (a 1) ^ 2
  | 2, 3 => -(a 4) * (a 5) + (a 2) * (a 5) + (a 2) * (a 4) - 2 * (a 2) * (a 3) - (a 2) ^ 2 + (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) + (a 0) * (a 2) - (a 0) * (a 1)
  | 2, 4 => -(a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) - 2 * (a 1) * (a 4) + (a 1) * (a 3) + (a 1) * (a 2) - (a 1) ^ 2 + (a 0) * (a 5) - (a 0) * (a 2) + (a 0) * (a 1)
  | 3, 0 => (a 2) * (a 3) * (a 4) - (a 2) ^ 2 * (a 3) - (a 1) * (a 4) ^ 2 + (a 1) * (a 2) * (a 4) + (a 0) * (a 4) * (a 5) + (a 0) * (a 2) * (a 5) - 2 * (a 0) * (a 2) * (a 4) + (a 0) * (a 2) * (a 3) + (a 0) * (a 1) * (a 4) - (a 0) ^ 2 * (a 5)
  | 3, 1 => (a 4) * (a 5) - (a 4) ^ 2 + (a 3) * (a 4) - (a 2) * (a 5) + (a 2) * (a 4) + (a 2) * (a 3) - 2 * (a 1) * (a 4) + (a 0) * (a 5) + (a 0) * (a 4) - (a 0) * (a 3)
  | 3, 2 => -(a 4) * (a 5) + (a 2) * (a 5) + (a 2) * (a 4) - 2 * (a 2) * (a 3) - (a 2) ^ 2 + (a 1) * (a 4) + (a 1) * (a 2) + (a 0) * (a 5) + (a 0) * (a 2) - (a 0) * (a 1)
  | 3, 3 => (a 4) ^ 2 - 2 * (a 2) * (a 4) + (a 2) ^ 2 - 2 * (a 0) * (a 4) - 2 * (a 0) * (a 2) + (a 0) ^ 2
  | 3, 4 => -(a 3) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - (a 1) * (a 2) - 2 * (a 0) * (a 5) + (a 0) * (a 4) + (a 0) * (a 3) + (a 0) * (a 2) + (a 0) * (a 1) - (a 0) ^ 2
  | 4, 0 => -(a 2) * (a 3) ^ 2 + (a 1) * (a 3) * (a 4) + (a 1) * (a 2) * (a 3) - (a 1) ^ 2 * (a 4) + (a 0) * (a 3) * (a 5) + (a 0) * (a 2) * (a 3) + (a 0) * (a 1) * (a 5) + (a 0) * (a 1) * (a 4) - 2 * (a 0) * (a 1) * (a 3) - (a 0) ^ 2 * (a 5)
  | 4, 1 => (a 3) * (a 5) + (a 3) * (a 4) - (a 3) ^ 2 - 2 * (a 2) * (a 3) - (a 1) * (a 5) + (a 1) * (a 4) + (a 1) * (a 3) + (a 0) * (a 5) - (a 0) * (a 4) + (a 0) * (a 3)
  | 4, 2 => -(a 3) * (a 5) + (a 2) * (a 3) + (a 1) * (a 5) - 2 * (a 1) * (a 4) + (a 1) * (a 3) + (a 1) * (a 2) - (a 1) ^ 2 + (a 0) * (a 5) - (a 0) * (a 2) + (a 0) * (a 1)
  | 4, 3 => -(a 3) * (a 4) + (a 2) * (a 3) + (a 1) * (a 4) - (a 1) * (a 2) - 2 * (a 0) * (a 5) + (a 0) * (a 4) + (a 0) * (a 3) + (a 0) * (a 2) + (a 0) * (a 1) - (a 0) ^ 2
  | 4, 4 => (a 3) ^ 2 - 2 * (a 1) * (a 3) + (a 1) ^ 2 - 2 * (a 0) * (a 3) - 2 * (a 0) * (a 1) + (a 0) ^ 2
  | _, _ => 0
THEOREM hasDerivAt_cmCofactor3Poly_34_along_coord · IndisputableMonolith/Geometry/CofactorPolynomial.lean
hasDerivAt_cmCofactor3Poly_34_along_coord · IndisputableMonolith/Geometry/CofactorPolynomial.lean:985 
/-- Closed-form coordinate derivative of the `(3,4)` cofactor polynomial. -/
theorem hasDerivAt_cmCofactor3Poly_34_along_coord
    (k : Fin 6) (a : SqEdges) :
    HasDerivAt (fun t : ℝ => cmCofactor3Poly 3 4 (Function.update a k t))
      (cmCofactorPartial 3 4 k a) (a k) := by
  have hfun :
      (fun t : ℝ => cmCofactor3Poly 3 4 (Function.update a k t)) =
        (fun t : ℝ => cmCofactor3Poly 3 4 a
          + cmCofactorPartial 3 4 k a * (t - a k)
          + (if k = 0 then -1 else 0) * (t - a k) ^ 2
          + 0 * (t - a k) ^ 3) := by
    funext t
    have h := cmCofactor3Poly_34_update_polyform 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 3 4 a)
    (cmCofactorPartial 3 4 k a) (if k = 0 then -1 else 0) 0 (a k)
THEOREM cmCofactor3_eq_poly · IndisputableMonolith/Geometry/CofactorPolynomial.lean
cmCofactor3_eq_poly · IndisputableMonolith/Geometry/CofactorPolynomial.lean:858 
/-- 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 declaration proves no new geometric fact about tetrahedra, such as a volume or angle formula. The declaration does not involve the golden ratio or the framework's forcing chain. The declaration does not define a derivative; it names a polynomial and a separate theorem proves the derivative result.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND