CofactorPolynomialAgreement
plain-language theorem explainer
The audit proposition that every tetrahedral Cayley–Menger cofactor, computed as a signed minor determinant on squared edge lengths, equals its expanded explicit polynomial in the six edge-square coordinates. Geometry and dihedral-angle developers cite it as the single named target that the per-entry normal-form lemmas discharge. It is a pure Prop definition, not a proved theorem.
Claim. For every assignment $a$ of the six squared edge lengths of a tetrahedron, and every row–column index pair $(r,c)\in\{0,\ldots,4\}^2$, the signed Cayley–Menger cofactor of $a$ at $(r,c)$ equals the corresponding explicit polynomial in those six squared lengths.
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates. It is the cofactor analogue of the derivative module: downstream dihedral-angle calculus can name polynomial partials instead of opaque Fréchet derivatives.
The Cayley–Menger matrix encodes squared distances among four points (plus a bordering row/column of ones) so that volume and dihedral data are determinants and cofactors of that matrix. Here cmCofactor3 is the determinant-based signed minor; cmCofactor3Poly is the hand-expanded polynomial normal form in the six edge-square slots (SqEdges).
The doc-comment states the design split: formulas are separated from the determinant proof because normalizing all Fin.succAbove minor cases in one theorem is too slow for interactive builds. Sibling lemmas such as the (3,4) and (2,4) cofactor–polynomial equalities discharge individual entries toward this global agreement proposition.
proof idea
No proof body: the declaration is a def whose right-hand side is the universal proposition
$\forall a,,r,,c.;\mathrm{cmCofactor3}(a,r,c)=\mathrm{cmCofactor3Poly}(r,c,a)$.
It packages the audit target that the per-minor polynomial lemmas (e.g. equality of the (3,4) and (2,4) cofactors with their expanded forms, via explicit $3\times3$ minor matrices and their determinants) are meant to establish entrywise. Heartbeat limits and case splits live in those sibling theorems, not here.
why it matters
In Recognition geometry, dihedral angles of the tetrahedron are recovered from Cayley–Menger cofactors. Naming a single agreement proposition lets the framework treat the explicit polynomials as interchangeable with determinant cofactors, so partial derivatives used in angle calculus stay algebraic rather than opaque fderiv terms.
The module doc positions this as the cofactor twin of the Cayley–Menger derivative layer. No downstream consumers are wired yet (used_by is empty), so the declaration is presently an audit interface: once every entry lemma is proved, a future theorem can inhabit this Prop and close the normal-form gap called out in the doc-comment.
It does not itself touch the forcing chain (T5–T8), RCL, or the phi ladder; it is local Euclidean scaffolding that those continuum limits may later quote when rigid tetrahedral geometry is needed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.