18.10. Cross-references🔗

Where HexGF2 fits in the executable DAG:

• HexPoly is the only dependency: it provides the generic dense-polynomial vocabulary against which the packed representation's arithmetic and Euclidean laws are stated. HexGF2 specializes that theory to the single-bit-coefficient case where the packed word layout and carry-less multiply apply.

• HexGF2 is consumed by the finite-field constructors that build on it (the packed characteristic-two entries of the GFq constructors), which reuse its Hex.GF2n and Hex.GF2nPoly wrappers and committed irreducibility certificates.

• HexGF2 is Mathlib-free. Its Mathlib correspondence is HexGF2Mathlib, which unpacks GF2Poly into the generic FpPoly 2 representation, identifies both GF2n and GF2nPoly with the quotient-field construction from HexGFqField, and carries the finiteness and cardinality results for the packed types. The executable API documented above does not depend on it: the packed arithmetic, the Euclidean algorithms, and the Rabin certificates are all executable and Mathlib-free.