3.1. Introduction🔗

HexMvPoly provides canonical sparse multivariate polynomials in a fixed number of variables. A polynomial stores its nonzero coefficients in monomial order, so equality is structural, iteration is ordered, and leading terms are available without sorting at each use. The monomial comparator is an explicit type parameter: callers can select lexicographic, graded lexicographic, or graded reverse lexicographic order.

The executable library is Mathlib-free. It depends on HexBasic for its tree-map and kernel-reduction support, and on HexPoly for the dense recursive view. HexMvPolyMathlib, described in the correspondence section, supplies the ring equivalence with Mathlib's multivariate polynomials and the proof-facing algebraic API.