17.1. Introduction🔗

HexGFq packages the committed Conway-table entries of HexConway as ready-to-use field types, so a caller who wants GF(pⁿ) for a supported pair (p, n) never has to supply a modulus or an irreducibility proof by hand. It builds on the executable field HexGFqField, the Conway lookup HexConway, and the packed characteristic-two field HexGF2.

It exposes two parallel families of constructors. The generic family builds every field as the HexGFqField quotient `Fₚ[x] / (f)` with f the committed Conway modulus, and works for every committed (p, n). The packed characteristic-two family, for committed binary entries, instead routes through the single-word HexGF2 representation, trading the generic quotient for machine-word arithmetic while certifying, at elaboration time, that the packed modulus is the same Conway polynomial. HexGFq is Mathlib-free. Everything below typechecks against the executable libraries only.