Encyclopedia Geometry Geometry Cofactor Polynomial Cm Cofactor3 Poly Update Polyform
ARTICLE 3 claims 3 theorems
Geometry Cofactor Polynomial Cm Cofactor3 Poly Update Polyform
A machine-checked library rewrites every tetrahedral geometry cofactor into an explicit polynomial in the six edge lengths, making derivative calculations concrete and checkable.
The polynomial form
In tetrahedral geometry, a Cayley-Menger matrix encodes the six edge lengths of a tetrahedron so that its determinant gives the squared volume. The cofactors of this matrix appear when you need angles between faces, and differentiating those angles with respect to an edge length is a standard but algebra-heavy task. A machine-checked library of formal theorems in the Recognition Science framework now provides an explicit polynomial normal form for every such cofactor: each one expands into a concrete polynomial in the six squared edge coordinates, instead of remaining an opaque matrix expression.
The central declaration, cmCofactor3Poly, defines this polynomial for any cofactor position in the 5 by 5 matrix. A companion theorem, cmCofactor3_eq_poly, proves that this polynomial equals the original cofactor for every choice of edge lengths and every matrix position. This is not a numerical approximation or a special case; it is an exact identity, checked by the library's kernel. The practical payoff is that downstream calculus can refer to named polynomial partial derivatives instead of wrestling with generic matrix derivative machinery.
The library also provides explicit partial derivatives. The theorem hasDerivAt_cmCofactor3Poly_along_coord states that the derivative of the polynomial with respect to one edge coordinate equals the corresponding named partial, cmCofactorPartial. This means that when a calculation needs the rate at which a dihedral angle changes as an edge stretches, it can call a ready-made polynomial derivative instead of re-deriving it from the matrix definition each time.
In Recognition Science, this is a piece of the framework's broader program: a machine-checked library of formal theorems that builds geometry from a discrete ledger of recognition events. The library's role here is to make an existing mathematical object, the Cayley-Menger cofactor, computationally explicit and formally verified. It does not introduce new physics or new geometry; it provides a verified computational tool for calculations that were previously done by hand or by less transparent means.
The declaration does not claim that these polynomials reveal new geometric facts, nor that they are the only possible normal form. It also does not claim that the framework's recognition ledger is needed to derive the Cayley-Menger formulas themselves; those are classical results. What it establishes is narrower and precise: a verified, explicit polynomial representation of every tetrahedral cofactor, ready for use in derivative calculations.
THEOREM cmCofactor3Poly · cmCofactor3_eq_poly · IndisputableMonolith/Geometry/CofactorPolynomial.lean
/-- 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
/-- 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
THEOREM cmCofactor3_eq_poly · IndisputableMonolith/Geometry/CofactorPolynomial.lean
/-- 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
THEOREM hasDerivAt_cmCofactor3Poly_along_coord · IndisputableMonolith/Geometry/CofactorPolynomial.lean
/-- 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
This declaration does not introduce new geometric facts or new physics. It does not claim that the polynomial normal form is unique or canonical. It does not claim that the framework's recognition ledger is required to derive the Cayley-Menger formulas.
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:
- How do these explicit polynomial cofactors simplify the derivation of dihedral angle formulas?
- What is the exact relationship between the Cayley-Menger matrix and the squared volume of a tetrahedron?
- Does the framework's ledger provide an independent derivation of the Cayley-Menger determinant itself?
- How do these polynomial partials compare in efficiency to generic automatic differentiation for tetrahedral geometry?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM cmCofactor3Poly · cmCofactor3_eq_poly · IndisputableMonolith/Geometry/CofactorPolynomial.lean
/-- 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/-- 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 aA machine-checked library of formal theorems in the Recognition Science framework now provides an explicit polynomial normal form for every such cofactor. cmCofactor3Poly · cmCofactor3_eq_poly · IndisputableMonolith/Geometry/CofactorPolynomial.leanTHEOREM cmCofactor3_eq_poly · IndisputableMonolith/Geometry/CofactorPolynomial.lean
/-- 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 aA companion theorem, cmCofactor3_eq_poly, proves that this polynomial equals the original cofactor for every choice of edge lengths and every matrix position. cmCofactor3_eq_poly · IndisputableMonolith/Geometry/CofactorPolynomial.leanTHEOREM hasDerivAt_cmCofactor3Poly_along_coord · IndisputableMonolith/Geometry/CofactorPolynomial.lean
/-- 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)The theorem hasDerivAt_cmCofactor3Poly_along_coord states that the derivative of the polynomial with respect to one edge coordinate equals the corresponding named partial, cmCofactorPartial. hasDerivAt_cmCofactor3Poly_along_coord · IndisputableMonolith/Geometry/CofactorPolynomial.lean