module module high

`IndisputableMonolith.Geometry.CofactorPolynomial`

Gives every tetrahedral Cayley-Menger cofactor an explicit multivariate polynomial normal form in the six edge lengths. Anyone differentiating dihedral cosines or matching cofactor identities to the 5x5 CM matrix cites this layer. The module builds the relevant 3x3 minors, expands their determinants as polynomials, and proves agreement with the matrix cofactors.

claimFor each entry of the $5\times 5$ Cayley-Menger matrix of a tetrahedron, the corresponding cofactor equals an explicitly written polynomial in the six squared edge lengths (e.g. the $(3,4)$ and $(2,4)$ cofactors match $\det$ of named $3\times 3$ minor matrices). Partial derivatives of those polynomials are likewise named.

background

The Cayley-Menger matrix encodes a tetrahedron's edge geometry so that volumes and dihedral data are determinants and cofactors. Upstream, CayleyMengerMatrix ties the explicit tetrahedral polynomial cm3 to the actual $5\times 5$ determinant and sets the row/column convention needed by the dihedral cosine formula. DihedralCayleyMenger then defines each edge's dihedral cosine from a ratio of those cofactors: for edge $(i,j)$ with opposite vertices $(p,q)$, the cosine is built from CM cofactors with vertex indices shifted by one in the bordered matrix.

This module sits between those layers and any calculus on dihedrals. It introduces named $3\times 3$ minor matrices (e.g. for positions $(3,4)$, $(2,4)$, $(2,3)$), their determinants as polynomials in the edge data, and a polynomial representative cmCofactor3Poly for each cofactor of interest, plus partials cmCofactorPartial. The agreement predicates record that the polynomial form equals the matrix cofactor.

proof idea

Definition-heavy module with targeted determinant expansions. For each needed cofactor index pair it builds an explicit minor matrix, proves the submatrix extraction identity against the full CM matrix, expands the $3\times 3$ determinant into a polynomial, and equates that polynomial to the corresponding CM cofactor. Agreement lemmas (cmCofactor3_34_eq_poly, cmCofactor3_24_eq_poly, and siblings) are the bridge from matrix language to polynomial language. Partials are defined on the polynomial side so later derivative interfaces need not differentiate determinants symbolically from scratch.

why it matters in Recognition Science

Dihedral cosines in Recognition geometry are cofactor ratios; any rigidity, variation, or continuum limit needs derivatives of those ratios. Downstream CofactorDerivatives imports this module to expose derivative hooks for CM cofactors and the dihedral cofactor ratio, noting that hard symbolic simplifications remain further down but the calculus layer is no longer implicit. Without polynomial normal forms, cofactor differentiation stays stuck in opaque matrix minors. This file is the algebraic normal-form step that makes those hooks honest and checkable against the Cayley-Menger determinant layer.

scope and limits

Does not derive the dihedral cosine formula itself; that lives upstream in DihedralCayleyMenger.
Does not simplify or evaluate symbolic derivatives of cofactor ratios; only supplies polynomial forms and partial hooks.
Does not treat higher simplices or non-tetrahedral Cayley-Menger matrices.
Does not prove geometric inequalities or positivity of volumes from the polynomials.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Geometry.CofactorDerivatives module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMengerMatrix module_import
IndisputableMonolith.Geometry.DihedralCayleyMenger module_import

declarations in this module (116)

def cmCofactor3Poly L27
def cmCofactorPartial L58
def CofactorPolynomialAgreement L204
def cmMinor34Matrix L210
theorem cmMinor34_submatrix_eq L218
theorem det_cmMinor34Matrix L225
theorem cmCofactor3_34_eq_poly L232
def cmMinor24Matrix L240
theorem cmMinor24_submatrix_eq L246
theorem det_cmMinor24Matrix L252
theorem cmCofactor3_24_eq_poly L258
def cmMinor23Matrix L265
theorem cmMinor23_submatrix_eq L271
theorem det_cmMinor23Matrix L277
theorem cmCofactor3_23_eq_poly L283
def cmMinor14Matrix L290
theorem cmMinor14_submatrix_eq L296
theorem det_cmMinor14Matrix L302
theorem cmCofactor3_14_eq_poly L308
def cmMinor13Matrix L315
theorem cmMinor13_submatrix_eq L321
theorem det_cmMinor13Matrix L327
theorem cmCofactor3_13_eq_poly L333
def cmMinor12Matrix L340
theorem cmMinor12_submatrix_eq L346
theorem det_cmMinor12Matrix L352
theorem cmCofactor3_12_eq_poly L358
def cmMinor11Matrix L365
theorem cmMinor11_submatrix_eq L371
theorem det_cmMinor11Matrix L377
theorem cmCofactor3_11_eq_poly L383
def cmMinor22Matrix L390
theorem cmMinor22_submatrix_eq L396
theorem det_cmMinor22Matrix L402
theorem cmCofactor3_22_eq_poly L408
def cmMinor33Matrix L415
theorem cmMinor33_submatrix_eq L421
theorem det_cmMinor33Matrix L427
theorem cmCofactor3_33_eq_poly L433
def cmMinor44Matrix L440
theorem cmMinor44_submatrix_eq L446
theorem det_cmMinor44Matrix L452
theorem cmCofactor3_44_eq_poly L458
theorem cmCofactor3_opposite_eq_poly L466
theorem cmCofactor3_opposite_diag_eq_poly L479
def cmMinor00Matrix L498
theorem cmMinor00_submatrix_eq L504
theorem det_cmMinor00Matrix L510
theorem cmCofactor3_00_eq_poly L516
def cmMinor01Matrix L522
theorem cmMinor01_submatrix_eq L528
theorem det_cmMinor01Matrix L534
theorem cmCofactor3_01_eq_poly L540
def cmMinor02Matrix L546
theorem cmMinor02_submatrix_eq L552
theorem det_cmMinor02Matrix L558
theorem cmCofactor3_02_eq_poly L564
def cmMinor03Matrix L570
theorem cmMinor03_submatrix_eq L576
theorem det_cmMinor03Matrix L582
theorem cmCofactor3_03_eq_poly L588
def cmMinor04Matrix L594
theorem cmMinor04_submatrix_eq L600
theorem det_cmMinor04Matrix L606
theorem cmCofactor3_04_eq_poly L612
def cmMinor10Matrix L618
theorem cmMinor10_submatrix_eq L624
theorem det_cmMinor10Matrix L630
theorem cmCofactor3_10_eq_poly L636
def cmMinor20Matrix L642
theorem cmMinor20_submatrix_eq L648
theorem det_cmMinor20Matrix L654
theorem cmCofactor3_20_eq_poly L660
def cmMinor21Matrix L666
theorem cmMinor21_submatrix_eq L672
theorem det_cmMinor21Matrix L678
theorem cmCofactor3_21_eq_poly L684
def cmMinor30Matrix L690
theorem cmMinor30_submatrix_eq L696
theorem det_cmMinor30Matrix L702

… and 36 more