1.8. Cross-references🔗

HexBasic has no dependencies: it imports only Lean and Std, and sits at the root of the library graph. Nothing depends on all of it, which is the point; each consumer takes the one or two modules it needs.

• The Std.ExtTreeMap merges are what HexMvPoly builds its canonical sparse representation on, with HexMvHensel reusing the same traversals.

• The kernel-reducible containers are taken by the libraries whose certificates are checked by decide +kernel over concrete arrays: HexMvPoly, HexSparsePoly, HexBerlekampZassenhaus, and HexRealRoots.

• The exact-division contract is shared by the fraction-free algorithms: HexResultant, HexMvGcd, and HexPolySmith each cancel a known nonzero factor through Hex.ExactDivLaws rather than carrying their own division hypothesis. HexBareiss solves the same problem one layer down, against HexArith.Int.exactDiv on a fixed carrier.

• The fold algebra travels with the multivariate stack, where sums are indexed by a map's keys: HexMvPoly, HexMvGcd, HexMvHensel, and HexResultant.

• HexBasic has no Mathlib companion, and needs none. Nothing here states a correspondence: these are Lean and Std facts that happen not to be upstream yet. The Mathlib bridges live in the consuming libraries' *Mathlib counterparts, which import both this library and Mathlib.